Theory SyntaxTest

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

(*<*)
theory SyntaxTest imports HeapList Vcg begin

record "globals" =
 alloc_' :: "ref list"
 free_':: nat
 GA_' :: "ref list list"
 next_' :: "ref ⇒ ref"
 cont_' :: "ref ⇒ nat"

record 'g vars = "'g state" +
  A_' :: "nat list"
  AA_' :: "nat list list"
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: int
  S_' :: int
  B_' :: bool
  Abr_':: string
  p_' :: ref
  q_' :: ref

procedures Foo (p,I|p) = "´p :== ´p"

term "´I :==⇩g 3 - 1"
term "´R :==⇩g 3 - 1"
term "´I :==⇩g ´A!i"
term " ´A!i :== j"
term " ´AA :== ´AA!![i,j]"
term " ´AA!![i,j] :== ´AA"
term "´A!i :==⇩g j"
term "´p :==⇩g ´GA!i!j"
term "´GA!i!j :==⇩g ´p"
term "´p :==⇩g ´p → ´next"
term "´p → ´next :==⇩g ´p"
term "´p → ´next → ´next :==⇩g ´p"
term "´p :== NEW sz [´next :== Null,´cont :== 0]"
term "´p→´next :==⇩g NEW sz [´next :== Null,´cont :== 0]"
term "´p :== NNEW sz [´next :== Null,´cont :== 0]"
term "´p→´next :==⇩g NNEW sz [´next :== Null,´cont :== 0]"
term "´B :==⇩g ´N + 1 < 0 ∧ ´M + ´N < n"
term "´B :==⇩g ´N + 1 < 0 ∨  ´M + ´N < n"
term "´I :==⇩g ´N mod n"
term "´I :==⇩g ´N div n"
term "´R :==⇩g ´R div n"
term "´R :==⇩g ´R mod n"
term "´R :==⇩g ´R * n"
term "´I :==⇩g ´I - ´N"
term "´R :==⇩g ´R - ´S"
term "´R :==⇩g int ´I"
term "´I :==⇩g nat ´R"
term "´R :==⇩g -´R"
term "IF⇩g ´A!i < ´N THEN c1 ELSE c2 FI"
term "WHILE⇩g ´A!i < ´N DO c OD"
term "WHILE⇩g ´A!i < ´N INV ⦃foo⦄ DO c OD"
term "WHILE⇩g ´A!i < ´N INV ⦃foo⦄ VAR bar x DO c OD"
term "WHILE⇩g ´A!i < ´N INV ⦃foo⦄ VAR bar x DO c OD;;c"
term "c;;WHILE⇩g ´A!i < ´N INV ⦃foo⦄ VAR MEASURE ´N + ´M DO c;;c OD;;c"
context Foo_impl
begin
term "´q :== CALL Foo(´p,´M)"
term "´q :== CALL⇩g Foo(´p,´M + 1)"
term "´q :== CALL Foo(´p→´next,´M)"
term "´q → ´next :== CALL Foo(´p,´M)"
end

end

(*>*)