Quelle  SyntaxTest.thy   Sprache: Isabelle

(*
    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 "\<acute>p\<rightarrow>\<acute>next :==\<^sub>g NEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
term "\<acute>p :== NNEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
term "\<acute>p\<rightarrow>\<acute>next :==\<^sub>g NNEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
term "\<acute>B :==\<^sub>g \<acute>N + 1 < 0 \<and> \<acute>M + \<acute>N < n"
term "\<acute>B :==\<^sub>g \<acute>N + 1 < 0 \<or>  \<acute>M + \<acute>N < n"
term "\<acute>I :==\<^sub>g \<acute>N mod n"
term "\<acute>I :==\<^sub>g \<acute>N div n"
term "\<acute>R :==\<^sub>g \<acute>R div n"
term "\<acute>R :==\<^sub>g \<acute>R mod n"
term "\<acute>R :==\<^sub>g \<acute>R * n"
term "\<acute>I :==\<^sub>g \<acute>I - \<acute>N"
term "\<acute>R :==\<^sub>g \<acute>R - \<acute>S"
term "\<acute>R :==\<^sub>g int \<acute>I"
term "\<acute>I :==\<^sub>g nat \<acute>R"
term "\<acute>R :==\<^sub>g -\<acute>R"
term "IF\<^sub>g \<acute>A!i < \<acute>N THEN c1 ELSE c2 FI"
term "WHILE\<^sub>g \<acute>A!i < \<acute>N DO c OD"
term "WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> DO c OD"
term "WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> VAR bar x DO c OD"
term "WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> VAR bar x DO c OD;;c"
term "c;;WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> VAR MEASURE \<acute>N + \<acute>M DO c;;c OD;;c"
context Foo_impl
begin
term "\<acute>q :== CALL Foo(\<acute>p,\<acute>M)"
term "\<acute>q :== CALL\<^sub>g Foo(\<acute>p,\<acute>M + 1)"
term "\<acute>q :== CALL Foo(\<acute>p\<rightarrow>\<acute>next,\<acute>M)"
term "\<acute>q \<rightarrow> \<acute>next :== CALL Foo(\<acute>p,\<acute>M)"
end

end

(*>*)