theory week09A_demo imports "~~/src/HOL/Hoare/HeapSyntax" begin primrec fac :: "nat \ nat" where "fac 0 = 1" | "fac (Suc n) = (Suc n) * fac n" lemma "VARS B { True } B := x { B = x }" sorry lemma " VARS (x::nat) y r {True} IF x>y THEN r:=x ELSE r:=y FI {r\x \ r \y \ (r=x \ r=y)}" sorry lemma "VARS (A::int) B { A = 0 \ B = 0 } WHILE A \ a INV { B = A * b} DO B := B + b; A := A + 1 OD {B = a * b }" sorry lemma factorial_sound: "VARS A B { A = n} B := 1; WHILE A \ 0 INV { fac n = B * fac A } DO B := B * A; A := A - 1 OD { B = fac n }" sorry \ \----------------------------------------------------------------------------------\ \ \Arrays\ (* define a program that looks for a key in an array *) (*think about the loop invariant *) term take lemma "VARS I L { True } I := 0; WHILE I < length L \ L!I \ key INV { TODO } DO I := I+1 OD { (I < length L \ L!I = key) \ (I=length L \ key \ set L)}" sorry \ \Pointers\ thm List_def Path.simps (* "List nxt p Ps" represents a linked list, starting at pointer p, with 'nxt' being the function to find the next pointer, and Ps the list of all the content of the linked list *) (* define a function that takes X, p and nxt function, assuming that X is in the set of the linked list, then it returns the pointer to that element *) (* think about its loop invariant *) (* because we are updating p itself, it is hard to state that X is not in the set of the path segment that we have already looked at. Instead we state the existence of the remaining segment that should include X *) lemma "VARS nxt p { List nxt p Ps \ X \ set Ps } WHILE p \ Null \ p \ Ref X INV { TODO } DO p := p^.nxt OD { p = Ref X }" sorry (* if we don't assume that X is in the set of the linked list, we need to change the the invariant and postconditions as follows *) lemma "VARS nxt p { List nxt p Ps } WHILE p \ Null \ p \ Ref X INV { TODO } DO p := p^.nxt OD { ( X \ set Ps \ p = Ref X) \ (\ X \ set Ps \ p = Null) }" sorry (* define a function that "splices" 2 disjoint linked lists together *) (* think about its loop invariant *) (* lemma "VARS tl p q pp qq {List tl p Ps \ List tl q Qs \ set Ps \ set Qs = {} \ size Qs \ size Ps} pp := p; WHILE q \ Null INV { TODO } DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD {List tl p (splice Ps Qs)}" sorry *) end