equal
deleted
inserted
replaced
|
1 (* Title: HOL/Hoare/Pointer_ExamplesAbort.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2002 TUM |
|
5 |
|
6 Examples of verifications of pointer programs |
|
7 *) |
|
8 |
|
9 theory Pointer_ExamplesAbort = HeapSyntaxAbort: |
|
10 |
|
11 section "Verifications" |
|
12 |
|
13 subsection "List reversal" |
|
14 |
|
15 text "Interestingly, this proof is the same as for the unguarded program:" |
|
16 |
|
17 lemma "VARS tl p q r |
|
18 {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}} |
|
19 WHILE p \<noteq> Null |
|
20 INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and> |
|
21 rev ps @ qs = rev Ps @ Qs} |
|
22 DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD |
|
23 {List tl q (rev Ps @ Qs)}" |
|
24 apply vcg_simp |
|
25 apply fastsimp |
|
26 apply(fastsimp intro:notin_List_update[THEN iffD2]) |
|
27 apply fastsimp |
|
28 done |
|
29 |
|
30 end |