src/HOL/Hoare/Pointer_ExamplesAbort.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 44890 22f665a2e91c permissions -rw-r--r--
executable domain membership checks
```     1 (*  Title:      HOL/Hoare/Pointer_ExamplesAbort.thy
```
```     2     Author:     Tobias Nipkow
```
```     3     Copyright   2002 TUM
```
```     4
```
```     5 Examples of verifications of pointer programs
```
```     6 *)
```
```     7
```
```     8 theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin
```
```     9
```
```    10 section "Verifications"
```
```    11
```
```    12 subsection "List reversal"
```
```    13
```
```    14 text "Interestingly, this proof is the same as for the unguarded program:"
```
```    15
```
```    16 lemma "VARS tl p q r
```
```    17   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
```
```    18   WHILE p \<noteq> Null
```
```    19   INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
```
```    20                  rev ps @ qs = rev Ps @ Qs}
```
```    21   DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
```
```    22   {List tl q (rev Ps @ Qs)}"
```
```    23 apply vcg_simp
```
```    24   apply fastforce
```
```    25  apply(fastforce intro:notin_List_update[THEN iffD2])
```
```    26 apply fastforce
```
```    27 done
```
```    28
```
```    29 end
```