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