Quelle  SyntaxTest.thy

(*
    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

(*>*)