21:I[90314,["https://schon.au/_next/static/immutable/chunks/1x5cg2pe3x4d1.js","https://schon.au/_next/static/immutable/chunks/2bhq7tnhs7omt.js","https://schon.au/_next/static/immutable/chunks/32ncs441skyll.js","https://schon.au/_next/static/immutable/chunks/1t10en_fq84vd.js","https://schon.au/_next/static/immutable/chunks/2099jd3bkl7bl.js","https://schon.au/_next/static/immutable/chunks/3e1nstitxnajz.js"],"default"] 22:I[72436,["https://schon.au/_next/static/immutable/chunks/1x5cg2pe3x4d1.js","https://schon.au/_next/static/immutable/chunks/2bhq7tnhs7omt.js","https://schon.au/_next/static/immutable/chunks/32ncs441skyll.js","https://schon.au/_next/static/immutable/chunks/1t10en_fq84vd.js","https://schon.au/_next/static/immutable/chunks/2099jd3bkl7bl.js","https://schon.au/_next/static/immutable/chunks/3e1nstitxnajz.js"],"Separator"] 23:I[86022,["https://schon.au/_next/static/immutable/chunks/1x5cg2pe3x4d1.js","https://schon.au/_next/static/immutable/chunks/2bhq7tnhs7omt.js","https://schon.au/_next/static/immutable/chunks/32ncs441skyll.js","https://schon.au/_next/static/immutable/chunks/1t10en_fq84vd.js","https://schon.au/_next/static/immutable/chunks/2099jd3bkl7bl.js","https://schon.au/_next/static/immutable/chunks/3e1nstitxnajz.js"],"default"] 24:T3a07,## Linear Sort ### 1. Mystery Sort **Example.** Sorting algorithm (no code, verification only) ```Dafny predicate sorted(a:array) reads a { forall j,k :: 0<=j a[j]<=a[k] } method MysterySort(a:array) modifies a ensures sorted(a) ensures multiset(a[..]) == multiset(old(a[..])) { // Sort code } method Validate() { var a := new int[][3,5,1,4]; assert a[0]==3 && a[1]==5 && a[2]==1 && a[3]==4; MysterySort(a); assert ms == multiset(a[..]); } ``` ### 2. Zero Sort Arrange an array of integers so all zeros are upfront. - Must be *in situ* - no other data structure allowed - Must be linear - May be unstable - order of non-zero elements is allowed to change **Example.** Zero sort returning number of zeros ```Dafny method ZeroSort(a:array) returns (nonz:int) modifies a ensures 0 <= nonbz <= a.Length // in range ensures forall i:: 0 <= i < nonz ==> a[i] == 0 // zero below ensures forall i:: nonz <= i < a.Length ==> a[i] != 0 // nonzero above ensures multiset(a[..]) == multiset(old(a[..])) { // Returns number of zeros nonz := 0; var next := 0; while next < a.Length invariant 0 <= nonz <= next <= a.Length // in range invariant forall i:: 0 <= i < nonz ==> a[i] == 0 // zero below invariant forall i:: nonz <= i < next ==> a[i] != 0 // nonzero above invariant multiset(a[..]) == multiset(old(a[..])) { if (a[next]==0) { a[next], a[nonz] := a[nonz], a[next]; nonz := nonz+1; // Increment nonz whenever zero is found at 'next' } next := next+1; // Increment next every iteration } } ``` > [!INFO] Specification > ==We only swap elements.== > - **Postcondition** > - The multiset of the **whole array** must remain the same on conclusion > `ensures multiset(a[..]) == multiset(old(a[..]))` > - **Invariant** > - Each swap in the loop does not change the multiset of the array > `invariant multiset(a[..]) == multiset(old(a[..]))` #### No Returns **Example.** Zero sort with no returns ```Dafny predicate zerosfirst(a:array) reads a { forall i,j:: ( 0<=i i) modifies a ensures zerosfirst(a) ensures multiset(a[..]) == multiset(old(a[..])) { var nonz := 0; var next := 0; while next < a.Length invariant 0 <= nonz <= next <= a.Length invariant forall i:: 0 <= i < nonz ==> a[i] == 0 invariant forall i:: nonz <= i < next ==> a[i] != 0 invariant multiset(a[..]) == multiset(old(a[..])) { if (a[next]==0) { a[next], a[nonz] := a[nonz], a[next]; nonz := nonz+1; } next := next+1; } } ``` #### Testing ![[Pasted image 20251109161740.png|500]] #### Validation ![[Pasted image 20251109161802.png|500]] #### Stability In the validator we cannot assert real data because the postcondition of `ZeroSort` is too weak. - The postcondition specifies that all zeros (if any) appear first - But the ==order of the non-zero elements may change== - `ZeroSort[1,0,2]` results in `[0,1,2]` - order of non-zeros is preserved - `ZeroSort[1,2,0]` results in `[0,2,1]` - order of non-zeros is not preserved **==It's unstable.==** ### 3. Dijkstra Sort #### The Dutch-Flag Problem > [!INFO] Dijkstra Strategy > All the balls are unsorted in an array. > Partition the array into four sections. > - Red section, initially empty > - White section, initially empty > - Unsorted section, initially the whole array > - Blue section, initially empty > > Use three pointers. > - White: start of white balls (initially 0) > - Next: start of unsorted balls (initially 0) > - Blue: start of blue balls (initially `array.Length`) > > ![[Pasted image 20251109162723.png|500]] - It is a linear sorting algorithm, just like `ZeroSort` is linear - The array is sored *in situ* - no other data structure used - Balls are swapped and the indexes updated each iteration - The algorithm terminates when indexes `next==blue` > [!QUESTION] > Given array `a` of coloured balls, and indexes `white` and `next==blue`. > > How many red balls will there be? `white` > How many white balls will there be? `blue - white` > How many blue balls will there be? `a.Length - blue` **Example.** Dijkstra strategy ```Dafny datatype Colour = RED | WHITE | BLUE method FlagSort(flag:array) returns (white:int, blue:int) modifies flag ensures 0 <= white <= blue <= flag.Length ensures forall i:: 0 <= i < white ==> flag[i] == RED ensures forall i:: white <= i < blue ==> flag[i] == WHITE ensures forall i:: blue <= i < flag.Length ==> flag[i] == BLUE ensures multiset(flag[..]) == multiset(old(flag[..])) { var next := 0; white := 0; blue := flag.Length; while next != blue invariant 0 <= white <= next <= blue <= flag.Length invariant forall i:: 0 <= i < white ==> flag[i] == RED invariant forall i:: white <= i < next ==> flag[i] == WHITE invariant forall i:: blue <= i < flag.Length ==> flag[i] == BLUE invariant multiset(flag[..]) == multiset(old(flag[..])) { match (flag[next]) { case RED => flag[next], flag[white] := flag[white], flag[next]; next := next+1; white := white+1; case WHITE => next := next+1; case BLUE => blue := blue-1; flag[next], flag[blue] := flag[blue], flag[next]; } } } ``` #### Predicates ![[Pasted image 20251109165311.png|500]] #### Testing ![[Pasted image 20251109165328.png|500]] #### Validation ![[Pasted image 20251109165344.png|500]] > [!NOTE] Remember > - Multiset `ms` and predicates `reds()`, `whites()`, `blues()` are ghosts > - The variables `size`, `flag[]`, `w` and `b` cannot be ghosts as they are compiled *** ## Quadratic Sort ### 1. Insertion Sort - There is a 'marker' index - Consider arrays of length $\geq 2$ only - Every 'iteration', move a card from unordered to ordered part The array `a` initially contains the elements to be sorted. - Precondition `requires a.Length >= 2` - Postcondition `ensures sorted(a, 0, a.Length)` `ensures multiset(a[..]) == multiset(old(a[..]))` - The predicate allows bounds to be placed on the sorted part `predicate sorted(a:array, low:int, high:int) reads a` `requires 0<=low<=high<=a.Length` `{ forall j,k:: low <= j < k < high ==> a[j] <= a[k] }` ### 2. Shuffle vs Swap When we 'add' a new element to the ordered part: > [!INFO] Shuffle > Shuffle each ordered element to the right (overwrites this element) > ...until the correct position is found to insert the new element > [!INFO] Swap > Swap each element in the ordered part with the new element > ...until the new element is in the correct position ![[Pasted image 20251109171100.png|center|500]] ### 3. Swap Insertion Sort #### Raw Code ```Dafny // Initially a[0] ordered, a[1..] unordered var up := 1; // 'up' is start of unordered while up= 1 && a[down-1] > a[down] { a[down-1], a[down] := a[down], a[down-1]; down := down-1; // decrement 'down' } up := up+1; // increment 'up' } ``` #### Outer Loop ```Dafny method SwapInsertionSort(a:array) modifies a requries a.Length > 0 ensures sorted(a, 0, a.Length) ensures multiset(a[..]) == multiset(old(a[..])) { var up := 1; // the first unordered element is at index 1 while up [!IMPORTANT] Swaps don't change the multiset! > > ![[Pasted image 20251109172311.png|400]] #### Inner Loop - **Down** starts at **up** and ends at **1**, so: `invariant 0<=down<=up` - Multiset is the same as the outer loop (**swaps don't affect multisets**) ```Dafny var down := up; while down >= 1 && a[down-1] > a[down] invariant 0<=down<=up invariant forall i,j:: (0<=i a[i]<=a[j] invariant multiset(a[..]) == multiset(old(a[..])) { a[down-1], a[down] := a[down], a[down-1] down := down-1; } ``` ![[Pasted image 20251109172709.png|center|300]] #### Full Code ```Dafny predicate sorted(a:array, low:int, high:int) reads a requires 0<=low<=high<=a.Length { forall j,k:: low <= j < k < high ==> a[j]<=a[k] } method SwapInsertionSort(a:array) modifies a requries a.Length > 0 ensures sorted(a, 0, a.Length) ensures multiset(a[..]) == multiset(old(a[..])) { var up := 1; while up= 1 && a[down-1] > a[down] invariant 0<=down<=up invariant forall i,j:: (0<=i a[i]<=a[j] invariant multiset(a[..]) == multiset(old(a[..])) { a[down-1], a[down] := a[down], a[down-1] down := down-1; } up := up+1; } } ``` ### 4. Validation ![[Pasted image 20251109173318.png|500]] *** ## Lemma Introduction ### 1. Lemmas Lemma is a **synonym** for `ghost method` `lemma Name(x1:int)` is equivalent to `ghost method Name(x1:int)` Dafny 'learns' a property from a lemma. - The property is the spec (i.e. pre and post condition) - The proof of the property is the **lemma body** - A lemma often does not return data > [!INFO] Lemma vs Assert > A lemma is like a 'big' assert statement. > - The spec in the lemma is the property > - Dafny must be able to prove it correct > - Lemmas and asserts are both ghsots > - Lemmas can call each other, asserts can't **Example.** General form of a lemma ```Dafny lemma Name(x1:T1, ..., xn:Tn) requires P ensures Q // P ==> Q is the property { ... } // the proof ``` - **Before** you call the lemma: - Precondition P is true, so assert P is true - **After** you have called the lemma: - Postcondition Q is true, so assert Q is true - The **effect** of the lemma is: - `forall x1:T1, ..., xn:Tn :: P ==> Q` ### 2. Proof Levels A **Level 1** proof is a complete, mathematical proof. - Can consist of a series of **assert** statements - Each assert is a logical **step in the proof** of the postcondition - Each assert is **justified** with a comment - E.g. `assert (a*b)*c == a*(b*c); // law of associativity` **Level 0** - Any proof that is not Level 1 - This includes all empty-body 'proofs' such as `LemSumEven` ### 3. Fermat's Last Conjecture > [!INFO] Property > It is impossible to find positive integers $x,y$ and $z$ that satisfy the equation $x^n+y^n=z^n$ for integers $n\gt 2$. **Example.** Dafny cannot prove the property. ```Dafny lemma LemFermat(a:int, b:int, c:int) requires a>0 && b>0 && c>0 ensures !(a*a*a + b*b*b == c*c*c) { } ``` ### 4. If $n$ is odd then so is $n^2$ > [!INFO] Property > If $n$ is odd, then $n^2$ is odd for all integers $n$. **Example.** Dafny cannot prove the property. ```Dafny method WhatDoYouKnow() { var n:int := *; // for all n assert n%2==1 ==> (n*n)%2==1; // try it } ``` #### Lemma `LemNN2` **Example.** The lemma fails to verify. ```Dafny lemma LemNN2(n:int) ensures n%2==1 ==> (n*n)%2==1 // the property { } ``` Asserts and lemmas are **not the same**. - In a lemma, Dafny may apply proof techniques such as **induction** - A lemma allows Dafny to **isolate** a property from the rest of the program - The spec in a lemma provides a more **expressive power** then an assertion - In a lemma, you can provide a proof **Example.** Level 1 proof. ```Dafny lemma LemNN2(n:int) ensures n%2==1 ==> (n*n)%2==1 { if n%2==1 { var k := (n-1)/2; // n odd, so n-1 is even assert n == 2*k + 1; // make n subject assert n*n == (2*k + 1)*(2*k + 1); // square both sides assert n*n == 2*k*2*k + 2*2*k + 1; // expand assert n*n == 2*(k*2*k) + 2*(2*k) + 1; // associativity assert n*n == 2*(k*2*k + 2*k) + 1; // factor out 2, form 2X+1 assert (n*n)%2 == 1; // n*n is odd, QED } } ``` > [!IMPORTANT] Every step must be justified in a Level 1 proof #### Validation ```Dafny ghost method Validate() { var n:int := *; // for any integer n LemNN2(n); // prove the property assert n%2==1 ==> (n*n)%2==1; // check Dafny has learnt it } ``` ### 5. If $n$ is even then so is $n * m$ > [!INFO] Property > If $n$ and $m$ are integers and $n$ is even, then $n*m$ is also even. **Example.** The lemma fails to verify. ```Dafny lemma LemMulEven(m:int, n:int) ensures n%2==0 ==> (n*m)%2==0 { } ``` #### Level 0 ```Dafny lemma LemMulEven(m:int, n:int) ensures n%2==0 ==> (n*m)%2==0 { if n%2==0 { assert n*m == 2*(n/2 * m); } } ``` #### Level 1 ```Dafny lemma LemMulEven(m:int, n:int) ensures n%2==0 ==> (n*m)%2==0 { if n%2==0 { var q := n/2; // because n is even we can divide by 2 assert 2*q == 2*n/2; // multiply both sides by 2 assert 2*q == n; // cancel out 2 on RHS assert n*m == 2*q*m; // multiply both sides by m, reverse sides assert (n*m)%2 == 0; // RHS is a multiple of 2, hence even, QED } } ``` #### Breakpoints Insert `assert false` breakpoint and keep moving it line by line until you find where it hangs. ```Dafny lemma LemMulEven(m:int, n:int) ensures n%2==0 ==> (n*m)%2==0 { if n%2==0 { var q := n/2; // because n is even we can divide by 2 assert 2*q == 2*n/2; // multiply both sides by 2 assert 2*q == n; // cancel out 2 on RHS // assert false; assert n*m == 2*q*m; // multiply both sides by m, reverse sides // assert false; assert (n*m)%2 == 0; // RHS is a multiple of 2, hence even, QED } } ``` #### Lemma `LemMulEven` ```Dafny lemma LemMulEven(m:int, n:int) ensures n%2==0 ==> (n*m)%2==0 { if n%2==0 { var q := n/2; // because n is even we can divide by 2 assert 2*q == 2*n/2; // multiply both sides by 2 assert 2*q == n; // cancel out 2 on RHS assert n*m == 2*q*m; // multiply both sides by m, reverse sides assert n*m == 2*(q*m); // apply right associativity to RHS assert (n*m)%2 == 0; // RHS is a multiple of 2, hence even, QED } } ``` #### General Validation - Note lemma **almost always** involve **general validation** - Validating a property using testcases serves no purpose ![[Pasted image 20251109183512.png|400]] #### Antecedent or Precondition? The context will make it clear what the correct choice is. - Will all calling methods satisfy the precondition? Generally it's a matter of *design*: - If the property is **used a lot**, ==implication is often better== - If the **condition is complex**, a ==precondition is often better== ##### Hot and Cold Validation ![[Pasted image 20251109183935.png|500]] 19:["$","div",null,{"className":"min-h-screen h-full w-full px-8 pb-8 pt-16 space-y-12","children":[["$","div",null,{"className":"flex justify-between flex-col items-start space-y-6 md:items-center md:flex-row","children":[["$","div",null,{"className":"flex flex-col space-y-2","children":[["$","div",null,{"className":"flex items-center gap-2","children":[["$","$L16",null,{"ref":"$undefined","iconNode":[["path",{"d":"M6 22a2 2 0 0 1-2-2V4a2 2 0 0 1 2-2h8a2.4 2.4 0 0 1 1.704.706l3.588 3.588A2.4 2.4 0 0 1 20 8v12a2 2 0 0 1-2 2z","key":"1oefj6"}],["path",{"d":"M14 2v5a1 1 0 0 0 1 1h5","key":"wfsgrz"}],["path",{"d":"M10 9H8","key":"b1mrlr"}],["path",{"d":"M16 13H8","key":"t4e002"}],["path",{"d":"M16 17H8","key":"z1uh3a"}]],"className":"lucide-file-text h-8 w-8"}],["$","h1",null,{"className":"font-semibold text-4xl uppercase","children":"SENG2011"}]]}],["$","p",null,{"className":"text-muted-foreground flex flex-col","children":[["$","span",null,{"className":"capitalize","children":["UNSW 2025 - Trimester 3"," -"," ","week 8"]}],["$","span",null,{"className":"text-sm","children":"Images have been removed to avoid copyright."}]]}]]}],["$","div",null,{"className":"flex items-center gap-2","children":[["$","$L4",null,{"href":"/notes","className":"inline-flex items-center justify-center gap-2 whitespace-nowrap rounded-md text-sm font-medium transition-all disabled:pointer-events-none disabled:opacity-50 [&_svg]:pointer-events-none [&_svg:not([class*='size-'])]:size-4 shrink-0 [&_svg]:shrink-0 outline-none focus-visible:border-ring focus-visible:ring-ring/50 focus-visible:ring-[3px] aria-invalid:ring-destructive/20 dark:aria-invalid:ring-destructive/40 aria-invalid:border-destructive bg-secondary text-secondary-foreground shadow-xs hover:bg-secondary/80 h-9 px-4 py-2 has-[>svg]:px-3","children":[["$","$L16",null,{"ref":"$undefined","iconNode":[["path",{"d":"m12 19-7-7 7-7","key":"1l729n"}],["path",{"d":"M19 12H5","key":"x3x0zl"}]],"className":"lucide-arrow-left h-4 w-4"}]," Notes"]}],["$","$L21",null,{"categories":[],"courseId":"SENG2011","weekId":"week-8","resources":[{"title":"Week 1","file":"week-1"},{"title":"Week 2","file":"week-2"},{"title":"Week 3","file":"week-3"},{"title":"Week 4","file":"week-4"},{"title":"Week 5","file":"week-5"},{"title":"Week 7","file":"week-7"},{"title":"Week 8","file":"week-8"},{"title":"Week 9","file":"week-9"},{"title":"Week 10","file":"week-10"}]}]]}]]}],["$","div",null,{"className":"overflow-hidden","children":[["$","$L22",null,{"orientation":"horizontal"}],["$","$L23",null,{"markdown":"$24"}]]}]]}]