[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

CaplanHarandi95

  1. Joshua E Caplan & Mehdi T Harandi(*@cs.uiuc.edu)
  2. A Logical Framework for Software Proof Reuse [SamadzadehZand95] pp106-113
  3. =THEORY DEMO PROOF REUSE
  4. Hoare triples do not have referential transparency!
      Created a new quantifier to bind (and hide) program identifiers into a context and protect them from sustitution. deca;arations also bind identifiers (and so hide them).

      Assignment axiom:

    1. for_vars x( {P(t=>x[m])} x[m]:= t {P} ). Declaration axiom:
    2. for_vars x({ P and x[m]=e} C{Q})
    3. ---------------------------------------------------where x=y,x[m],z.
    4. for_vars y,z( {P} new x[m]:=e ; C {Q} )


Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]