8177
|
1 |
(* Title: HOL/IMPP/EvenOdd.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 1999 TUM
|
|
5 |
|
|
6 |
Example of mutually recursive procedures verified with Hoare logic
|
|
7 |
*)
|
|
8 |
|
|
9 |
EvenOdd = Misc +
|
|
10 |
|
|
11 |
constdefs even :: nat => bool
|
|
12 |
"even n == 2 dvd n"
|
|
13 |
|
|
14 |
consts
|
|
15 |
Even, Odd :: pname
|
|
16 |
rules
|
|
17 |
Even_neq_Odd "Even ~= Odd"
|
|
18 |
Arg_neq_Res "Arg ~= Res"
|
|
19 |
|
|
20 |
constdefs
|
|
21 |
evn :: com
|
|
22 |
"evn == IF (%s. s<Arg>=0)
|
|
23 |
THEN Loc Res:==(%s. 0)
|
|
24 |
ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
|
|
25 |
Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
|
|
26 |
Loc Res:==(%s. s<Res> * s<Arg>))"
|
|
27 |
odd :: com
|
|
28 |
"odd == IF (%s. s<Arg>=0)
|
|
29 |
THEN Loc Res:==(%s. 1)
|
|
30 |
ELSE(Loc Res:=CALL Even (%s. s<Arg> -1))"
|
|
31 |
|
|
32 |
defs
|
|
33 |
bodies_def "bodies == [(Even,evn),(Odd,odd)]"
|
|
34 |
|
|
35 |
consts
|
|
36 |
Z_eq_Arg_plus :: nat => nat assn ("Z=Arg+_" [50]50)
|
|
37 |
"even_Z=(Res=0)" :: nat assn ("Res'_ok")
|
|
38 |
defs
|
|
39 |
Z_eq_Arg_plus_def "Z=Arg+n == %Z s. Z = s<Arg>+n"
|
|
40 |
Res_ok_def "Res_ok == %Z s. even Z = (s<Res>=0)"
|
|
41 |
|
|
42 |
end
|