1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      SyntaxTest.thy
8    Author:     Norbert Schirmer, TU Muenchen
9
10Copyright (C) 2006-2008 Norbert Schirmer
11Some rights reserved, TU Muenchen
12
13This library is free software; you can redistribute it and/or modify
14it under the terms of the GNU Lesser General Public License as
15published by the Free Software Foundation; either version 2.1 of the
16License, or (at your option) any later version.
17
18This library is distributed in the hope that it will be useful, but
19WITHOUT ANY WARRANTY; without even the implied warranty of
20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21Lesser General Public License for more details.
22
23You should have received a copy of the GNU Lesser General Public
24License along with this library; if not, write to the Free Software
25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
26USA
27*)
28(*<*)
29theory SyntaxTest imports HeapList Vcg begin
30
31record "globals" =
32 alloc_' :: "ref list"
33 free_':: nat
34 GA_' :: "ref list list"
35 next_' :: "ref \<Rightarrow> ref"
36 cont_' :: "ref \<Rightarrow> nat"
37
38record 'g vars = "'g state" +
39  A_' :: "nat list"
40  AA_' :: "nat list list"
41  I_' :: nat
42  M_' :: nat
43  N_' :: nat
44  R_' :: int
45  S_' :: int
46  B_' :: bool
47  Abr_':: string
48  p_' :: ref
49  q_' :: ref
50
51procedures Foo (p,I|p) = "\<acute>p :== \<acute>p"
52
53term "\<acute>I :==\<^sub>g 3 - 1"
54term "\<acute>R :==\<^sub>g 3 - 1"
55term "\<acute>I :==\<^sub>g \<acute>A!i"
56term " \<acute>A!i :== j"
57term " \<acute>AA :== \<acute>AA!![i,j]"
58term " \<acute>AA!![i,j] :== \<acute>AA"
59term "\<acute>A!i :==\<^sub>g j"
60term "\<acute>p :==\<^sub>g \<acute>GA!i!j"
61term "\<acute>GA!i!j :==\<^sub>g \<acute>p"
62term "\<acute>p :==\<^sub>g \<acute>p \<rightarrow> \<acute>next"
63term "\<acute>p \<rightarrow> \<acute>next :==\<^sub>g \<acute>p"
64term "\<acute>p \<rightarrow> \<acute>next \<rightarrow> \<acute>next :==\<^sub>g \<acute>p"
65term "\<acute>p :== NEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
66term "\<acute>p\<rightarrow>\<acute>next :==\<^sub>g NEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
67term "\<acute>p :== NNEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
68term "\<acute>p\<rightarrow>\<acute>next :==\<^sub>g NNEW sz [\<acute>next :== Null,\<acute>cont :== 0]"
69term "\<acute>B :==\<^sub>g \<acute>N + 1 < 0 \<and> \<acute>M + \<acute>N < n"
70term "\<acute>B :==\<^sub>g \<acute>N + 1 < 0 \<or>  \<acute>M + \<acute>N < n"
71term "\<acute>I :==\<^sub>g \<acute>N mod n"
72term "\<acute>I :==\<^sub>g \<acute>N div n"
73term "\<acute>R :==\<^sub>g \<acute>R div n"
74term "\<acute>R :==\<^sub>g \<acute>R mod n"
75term "\<acute>R :==\<^sub>g \<acute>R * n"
76term "\<acute>I :==\<^sub>g \<acute>I - \<acute>N"
77term "\<acute>R :==\<^sub>g \<acute>R - \<acute>S"
78term "\<acute>R :==\<^sub>g int \<acute>I"
79term "\<acute>I :==\<^sub>g nat \<acute>R"
80term "\<acute>R :==\<^sub>g -\<acute>R"
81term "IF\<^sub>g \<acute>A!i < \<acute>N THEN c1 ELSE c2 FI"
82term "WHILE\<^sub>g \<acute>A!i < \<acute>N DO c OD"
83term "WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> DO c OD"
84term "WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> VAR bar x DO c OD"
85term "WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> VAR bar x DO c OD;;c"
86term "c;;WHILE\<^sub>g \<acute>A!i < \<acute>N INV \<lbrace>foo\<rbrace> VAR MEASURE \<acute>N + \<acute>M DO c;;c OD;;c"
87context Foo_impl
88begin
89term "\<acute>q :== CALL Foo(\<acute>p,\<acute>M)"
90term "\<acute>q :== CALL\<^sub>g Foo(\<acute>p,\<acute>M + 1)"
91term "\<acute>q :== CALL Foo(\<acute>p\<rightarrow>\<acute>next,\<acute>M)"
92term "\<acute>q \<rightarrow> \<acute>next :== CALL Foo(\<acute>p,\<acute>M)"
93end
94
95end
96
97(*>*)
98