equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 |
5 |
6 Some small examples for programs that may abort. |
6 Some small examples for programs that may abort. |
7 Currently only show the absence of abort. |
|
8 *) |
7 *) |
9 |
8 |
10 theory ExamplesAbort = HoareAbort: |
9 theory ExamplesAbort = HoareAbort: |
11 |
10 |
12 syntax guarded_com :: "'bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("_ \<rightarrow> _" 60) |
|
13 translations "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI" |
|
14 |
|
15 lemma "VARS x y z::nat |
11 lemma "VARS x y z::nat |
16 {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}" |
12 {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}" |
17 by vcg_simp |
13 by vcg_simp |
|
14 |
|
15 lemma |
|
16 "VARS a i j |
|
17 {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}" |
|
18 apply vcg_simp |
|
19 apply arith |
|
20 done |
18 |
21 |
19 lemma "VARS (a::int list) i |
22 lemma "VARS (a::int list) i |
20 {True} |
23 {True} |
21 i := 0; |
24 i := 0; |
22 WHILE i < length a |
25 WHILE i < length a |
23 INV {i <= length a} |
26 INV {i <= length a} |
24 DO i < length a \<rightarrow> a := a[i := 7]; |
27 DO a[i] := 7; i := i+1 OD |
25 i := i+1 |
|
26 OD |
|
27 {True}" |
28 {True}" |
28 apply vcg_simp |
29 apply vcg_simp |
29 apply arith |
30 apply arith |
30 done |
31 done |
31 |
32 |