src/HOL/Hoare/ExamplesAbort.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 42154 478bdcea240a
permissions -rw-r--r--
tuned: each session has at most one defining entry;
nipkow@13857
     1
(*  Title:      HOL/Hoare/ExamplesAbort.thy
nipkow@13857
     2
    Author:     Tobias Nipkow
nipkow@13857
     3
    Copyright   1998 TUM
nipkow@13857
     4
nipkow@13857
     5
Some small examples for programs that may abort.
nipkow@13857
     6
*)
nipkow@13857
     7
haftmann@35316
     8
theory ExamplesAbort imports Hoare_Logic_Abort begin
nipkow@13856
     9
nipkow@13856
    10
lemma "VARS x y z::nat
nipkow@13856
    11
 {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
nipkow@13856
    12
by vcg_simp
nipkow@13856
    13
nipkow@13875
    14
lemma
nipkow@13875
    15
 "VARS a i j
nipkow@13875
    16
 {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
wenzelm@42154
    17
by vcg_simp
nipkow@13875
    18
nipkow@13856
    19
lemma "VARS (a::int list) i
nipkow@13856
    20
 {True}
nipkow@13856
    21
 i := 0;
nipkow@13856
    22
 WHILE i < length a
nipkow@13856
    23
 INV {i <= length a}
nipkow@13875
    24
 DO a[i] := 7; i := i+1 OD
nipkow@13856
    25
 {True}"
wenzelm@42154
    26
by vcg_simp
nipkow@13856
    27
nipkow@13856
    28
end