src/HOL/Hoare/ExamplesAbort.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35316 870dfea4f9c0
child 42154 478bdcea240a
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     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 apply vcg_simp
    18 done
    19 
    20 lemma "VARS (a::int list) i
    21  {True}
    22  i := 0;
    23  WHILE i < length a
    24  INV {i <= length a}
    25  DO a[i] := 7; i := i+1 OD
    26  {True}"
    27 apply vcg_simp
    28 done
    29 
    30 end