src/HOL/Hoare/ExamplesAbort.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13875 12997e3ddd8d
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/Hoare/ExamplesAbort.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998 TUM
     5 
     6 Some small examples for programs that may abort.
     7 *)
     8 
     9 theory ExamplesAbort = HoareAbort:
    10 
    11 lemma "VARS x y z::nat
    12  {y = z & z \<noteq> 0} z \<noteq> 0 \<rightarrow> x := y div z {x = 1}"
    13 by vcg_simp
    14 
    15 lemma
    16  "VARS a i j
    17  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
    18 apply vcg_simp
    19 apply arith
    20 done
    21 
    22 lemma "VARS (a::int list) i
    23  {True}
    24  i := 0;
    25  WHILE i < length a
    26  INV {i <= length a}
    27  DO a[i] := 7; i := i+1 OD
    28  {True}"
    29 apply vcg_simp
    30 apply arith
    31 done
    32 
    33 end