isabelle: src/HOL/IMP/VC.thy@c4e16b36bc57

     1 (*  Title:      HOL/IMP/VC.thy

     2     ID:         $Id$

     3     Author:     Tobias Nipkow

     4     Copyright   1996 TUM

     6 acom: annotated commands

     7 vc:   verification-conditions

     8 awp:   weakest (liberal) precondition

     9 *)

    11 VC  =  Hoare +

    13 datatype  acom = Askip

    14                | Aass   loc aexp

    15                | Asemi  acom acom

    16                | Aif    bexp acom acom

    17                | Awhile bexp assn acom

    19 consts

    20   vc,awp :: acom => assn => assn

    21   vcawp :: "acom => assn => assn * assn"

    22   astrip :: acom => com

    24 primrec awp acom

    25   "awp Askip Q = Q"

    26   "awp (Aass x a) Q = (%s.Q(s[a s/x]))"

    27   "awp (Asemi c d) Q = awp c (awp d Q)"

    28   "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"

    29   "awp (Awhile b I c) Q = I"

    31 primrec vc acom

    32   "vc Askip Q = (%s.True)"

    33   "vc (Aass x a) Q = (%s.True)"

    34   "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"

    35   "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)"

    36   "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &

    37                               (I s & b s --> awp c I s) & vc c I s)"

    39 primrec astrip acom

    40   "astrip Askip = SKIP"

    41   "astrip (Aass x a) = (x:=a)"

    42   "astrip (Asemi c d) = (astrip c;astrip d)"

    43   "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"

    44   "astrip (Awhile b I c) = (WHILE b DO astrip c)"

    46 (* simultaneous computation of vc and awp: *)

    47 primrec vcawp acom

    48   "vcawp Askip Q = (%s.True, Q)"

    49   "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"

    50   "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;

    51                               (vcc,wpc) = vcawp c wpd

    52                           in (%s. vcc s & vcd s, wpc))"

    53   "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;

    54                               (vcc,wpc) = vcawp c Q

    55                           in (%s. vcc s & vcd s,

    56                               %s.(b s --> wpc s) & (~b s --> wpd s)))"

    57   "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I

    58                              in (%s. (I s & ~b s --> Q s) &

    59                                      (I s & b s --> wpc s) & vcc s, I))"

    61 end

author	nipkow
	Tue Mar 18 18:02:19 1997 +0100 (1997-03-18)
changeset 2810	c4e16b36bc57
parent 1900	c7a869229091
child 3842	b55686a7b22c
permissions	-rw-r--r--