Automating Refinement of Circus Programs - Formal Methods: Foundations and Applications - page 284

This shape is similar to that of rephrased laws, but additionally includes the
provisos p i ∈ . We explain below how they are discarded

during the application of the tactic. We use

T for all i ∈{ 1 ,..., n }

, the structural combinator for in-
ternal choice, as an example. The approach applies to all unary, binary and n-ary
combinators of the ArcAngel C program model. An exception is the combinator

μ for recursion, which we address separately.
The combinator

internal choice has the following monotonicity
theorem in our original implementation. (There are no fixed arguments.)

for Circus

p 1 , p 2 , p 1 , p 2 : CIRCUS ACTION ∀ | α p 1 = α p 2 •

p 1 ∧ p 2 ⇒ p 1 C p 2 p 1 p 2 p 1 C p 2

Besides the type provisos, we require with α p 1 = α p 2 that p 1 and p 2 have
the same alphabet. This is crucial for the well-definedness of p 1 C p 2 .The
refinements in the antecedent imply that α p 1 = α p 1 and α p 2 = α p 2 , hence
we can conclude that α p 1 = α p 2 holds too. This ensures well-definedness of
p 1 C p 2 . Accordingly, the new monotonicity theorem is as follows.

∀

p 1 , p 2 :

U

; p 1 , p 2 :

U |

wd ( p 1 C p 2 )

∧

p 1 ∈

∧

CIRCUS ACTION

p 2 ∈

•

CIRCUS ACTION

p 1 ∧ p 2 ⇒ p 1 C p 2 ∧ wd ( p 1 C p 2 )

p 1 p 2 p 1 C p 2

We observe that we cannot rid ourselves of all type provisos: membership of p 1
and p 2 to CIRCUS ACTION stays, because refinement of p 1 and p 2 does not
necessarily preserve membership to CIRCUS ACTION .Wecan,however,usea
proof tactic to remove these provisos in the resulting theorem by proving them
from the residual assumptions and again using the cut rule as follows.
When a structural combinator is applied, the first step is to dissect the op-
erator application and apply the combinator tactics to the program operands.
Here, for example, applying t 1 C B applies t 1 to A and t 2 to B .

This results in the refinement theorems Γ 1 , wd A

t 2 to A

A ∧ wd A and A

B ∧ wd B . We then conjoin these theorems to obtain

Γ 2 , wd B B

B whose conclusion has now the right
shape to apply the monotonicity theorem in a forward-chaining manner, that is,
using modus ponens to obtain the conclusion of the theorem. This yields

A ∧

Γ 1 , Γ 2 , wd A , wd B A B

Γ 1 , Γ 2 , A ∈ CIRCUS ACTION , B ∈

CIRCUS ACTION ,

A C B ∧ wd ( A C B ) .

wd A , wd B , wd ( A C B ) A C B

From the application of wd to the original program, in our example A C B ,itfol-

lows, by the definition of wd , that the operands are well-defined; in our example,
wd A and wd B hold, so both can be easily eliminated as before. For the elim-
ination of the assumptions related to the restrictions on the components of the
new program, that is, A ∈ CIRCUS ACTION and B ∈

CIRCUS ACTION
in the example above, we exploit the wd theorems of the individual program re-
finements. They are in the case above Γ 1 , wd A wd A and Γ 2 , wd B wd B .