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;
     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