isabelle: src/HOL/IMP/VC.thy@6803ecb9b198

     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 wp:   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,wp :: acom => assn => assn

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

    22   astrip :: acom => com

    24 primrec wp acom

    25   wp_Askip  "wp Askip Q = Q"

    26   wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"

    27   wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"

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

    29   wp_Awhile "wp (Awhile b I c) Q = I"

    31 primrec vc acom

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

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

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

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

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

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

    39 primrec astrip acom

    40   astrip_Askip  "astrip Askip = skip"

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

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

    43   astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"

    44   astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"

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

    47 primrec vcwp acom

    48   vcwp_Askip

    49   "vcwp Askip Q = (%s.True, Q)"

    50   vcwp_Aass

    51   "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))"

    52   vcwp_Asemi

    53   "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;

    54                             (vcc,wpc) = vcwp c wpd

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

    56   vcwp_Aif

    57   "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;

    58                             (vcc,wpc) = vcwp c Q

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

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

    61   vcwp_Awhile

    62   "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I

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

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

    66 end

author	nipkow
	Tue Jan 23 14:25:55 1996 +0100 (1996-01-23)
changeset 1451	6803ecb9b198
parent 1447	bc2c0acbbf29
child 1476	608483c2122a
permissions	-rw-r--r--