Refinement Laws

Strengthen Relation:

   pre /\ rel2  ==>  rel1
 -----------------------
     {pre} v:=v' | rel1
   [=
      {pre} v:=v' | rel2

Remove Conjunct:

    pre /\  rel1  ==>  rel2
 ---------------------------------
    {pre} v:=v' | rel1  /\  rel2
  [=
     {pre} v:=v' | rel1

Contract Frame:

     x,v:=x',v' | rel /\ x'=x
   [=
      v:=v' | rel[x'\x]

Weaken Assert:

     pre1  ==>  pre2
 -----------------------
     {pre1}
   [=
      {pre2}

Introduce Assert:

A)   E doesn't mention v
   -----------------------
       v:=E
    [=
        v:=E ; { v=E }

B)   post  doesn't mention v
   -------------------------------------
     v:=v' | post
    [=
        (v:=v' | post) ; { post[v'\v] }

Push Assert:

A)    {pre} v:=E
    [=
       v:=E; { (?v.pre) }

B)   pre doesn't mention v
   ----------------------
     {pre} v:=E
    [=
       v:=E; { pre }

C)    {pre} v:=v' | rel
    [=
       (v:=v' | rel) ; { (?v.pre) }

Merge Assert:

    {pre1} ; {pre2}   =   {pre1 /\ pre2}

Rewrite:

Let F[E1] be an expression containing an occurrence of subexpression E1. Then F[E2] is that expression with the occurrence of E1 replaced by E2.

A)    { E1=E2 } v:=F[E1]
    [=
       v:=F[E2]

B)   pre  ==>  E1=E2
  ---------------------
      { pre } v:=F[E1]
    [=
       v:=F[E2]

C)    { E1=E2 } v:=v' | rel[E1]
    [=
       v:=v' | rel[E2]

D)    v:=v' | E1=E2  /\  rel[E1]
    [=
       v:=v' | E1=E2  /\  rel[E2]

Remove Assert:

     {pre}
  [=
      skip

Introduce Assignment:

A)   x:=x' | x'=E
   [=
      x:=E

B)   pre  ==>  rel[x'\E]
  -----------------------
     {pre} x:=x' | rel
   [=
      x:=E

Introduce Sequential Composition:

   post  doesn't mention v
 ---------------------------------------
     v:=v' | post
  [=
      (v:=v' | post2)  ;   v:=v' | post

Introduce Leading Assignment:

      rel doesn't mention x
 -------------------------------------
     v,x:=v',x' | rel
   [=
      x:=E;  v,x:=v',x' | rel

Introduce Trailing Assignment:

      rel doesn't mention x'
      E doesn't mention v
 -------------------------------------
     v,x:=v',x' | rel /\ x'=E
  [=
      (v:=v' | rel)  ;   x:=E[v'\v]

Introduce IF-statement:

     {pre} v:=v' | rel
  [=
      IF  G
      THEN  {G /\ pre} v:=v' | rel
      ELSE  {~G /\ pre} v:=v' | rel

Remove IF-statement:

A)   {G} IF G THEN S ELSE T FI   =   {G} S

B)   {~G} IF G THEN S ELSE T FI   =   {~G} T

Introduce DO-statement:

In order to refine a specification statement into a DO-statement, we require three things:

A guard G, which determines the conditions under which we continue iterating.
A loop invariant inv, that should be true before entering the loop, and be strong enough to imply the required postcondition when we exit the loop. We shall require the invariant to remain true during execution of the loop.
A loop variant E to ensure that the loop terminates. The variant should be some expression with an integer value that is decremented at each iteration, but never goes below zero. To ensure loop termination, we shall require that the variant is decremented during each iteration.

We express the law as follows:

      post  doesn't mention v
      pre  ==>  inv
      inv /\ ~G  ==>  post[v'\v]
 -------------------------------------
     {pre} v:=v' | post
  [=
      DO  G  ->
        {inv /\ G} v:=v' | inv[v\v']  /\   0 <= E[v\v'] < E
      OD

Introduce Local Variable:

     {pre} v:=v' | rel
   [=
      VAR l:T . l:=E;  {pre} v,l:=v',l' | rel

Introduce Constant:

     {pre} v,x:=v',x' | rel      
   [=
      CON C:T | C=x . {C=x /\ pre} v,x:=v',x' | rel

Remove Constant:

   S doesn't mention C
 -----------------------
     CON C:T | C=x . S
   [=
      S