Up to index of Isabelle/HOL/Hoare
theory Pointer_ExamplesAbort(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy ID: $Id: Pointer_ExamplesAbort.thy,v 1.2 2005/06/17 14:13:07 haftmann Exp $ Author: Tobias Nipkow Copyright 2002 TUM Examples of verifications of pointer programs *) theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin section "Verifications" subsection "List reversal" text "Interestingly, this proof is the same as for the unguarded program:" lemma "VARS tl p q r {List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}} WHILE p ≠ Null INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧ rev ps @ qs = rev Ps @ Qs} DO r := p; (p ≠ Null -> p := p^.tl); r^.tl := q; q := r OD {List tl q (rev Ps @ Qs)}" apply vcg_simp apply fastsimp apply(fastsimp intro:notin_List_update[THEN iffD2]) apply fastsimp done end
lemma
{List tl p Ps ∧ List tl q Qs ∧ set Ps ∩ set Qs = {}} WHILE p ≠ Null INV {∃ps qs. List tl p ps ∧ List tl q qs ∧ set ps ∩ set qs = {} ∧ rev ps @ qs = rev Ps @ Qs} DO r := p; p ≠ Null -> p := tl (addr p); r ≠ Null -> tl := tl(r -> q); q := r OD {List tl q (rev Ps @ Qs)}