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