src/HOL/IMP/VC.thy
author nipkow
Wed Feb 07 12:22:32 1996 +0100 (1996-02-07)
changeset 1481 03f096efa26d
parent 1476 608483c2122a
child 1696 e84bff5c519b
permissions -rw-r--r--
Modified datatype com.
Added (part of) relative completeness proof for Hoare logic.
     1 (*  Title:      HOL/IMP/VC.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996 TUM
     5 
     6 acom: annotated commands
     7 vc:   verification-conditions
     8 wp:   weakest (liberal) precondition
     9 *)
    10 
    11 VC  =  Hoare +
    12 
    13 datatype  acom = Askip
    14                | Aass   loc aexp
    15                | Asemi  acom acom
    16                | Aif    bexp acom acom
    17                | Awhile bexp assn acom
    18 
    19 consts
    20   vc,wp :: acom => assn => assn
    21   vcwp :: "acom => assn => assn * assn"
    22   astrip :: acom => com
    23 
    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"
    30 
    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)"
    38 
    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) = (IF b THEN astrip c ELSE astrip d)"
    44   astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    45 
    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))"
    65 
    66 end