## 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
```

```

```