| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Hoare/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 842 B |
|
Quelle Pointer_ExamplesAbort.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy Author: Tobias Nipkow Copyright 2002 TUM *) section ‹Examples of verifications of pointer programs› theory Pointer_ExamplesAbort imports HeapSyntaxAbort begin subsection "Verifications" subsubsection "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 fastforce apply(fastforce intro:notin_List_update[THEN iffD2]) done end
¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26