src/HOL/Hoare/ExamplesAbort.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 42154 478bdcea240a
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 (*  Title:      HOL/Hoare/ExamplesAbort.thy
     2     Author:     Tobias Nipkow
     3     Copyright   1998 TUM
     4 
     5 Some small examples for programs that may abort.
     6 *)
     7 
     8 theory ExamplesAbort imports Hoare_Logic_Abort begin
     9 
    10 lemma "VARS x y z::nat
    11  {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
    12 by vcg_simp
    13 
    14 lemma
    15  "VARS a i j
    16  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
    17 by vcg_simp
    18 
    19 lemma "VARS (a::int list) i
    20  {True}
    21  i := 0;
    22  WHILE i < length a
    23  INV {i <= length a}
    24  DO a[i] := 7; i := i+1 OD
    25  {True}"
    26 by vcg_simp
    27 
    28 end