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

As already said, these well-definedness constraints give rise to proof obliga-
tions that accumulate through the application of ArcAngel C tactics. Sources for

the provisos are model theorems automatically applied in the mechanics of the
ArcAngel C

implementation, monotonicity theorems applied when invoking struc-
tural combinators, and user-defined laws. In practice, even after applying just the
first three of the seven phases of the refinement tactic NB for control laws [13],
the resulting theorem already includes more than 130 assumptions. Thereafter
it becomes unmanageable, slowing down or even bringing to a stall further ap-
plication of tactics. To tackle this problem we have pursued a combination of
two approaches. They are explained separately in the following sections.

3.1 Reducing Constraints in the Semantic Encoding

To tame the complexity of generated assumptions, we have used a novel treat-
ment of typing . This reduced the number of provisos but has retained soundness.
By way of illustration, the semantic function for ∧ is defined as follows.

( ∧ P ): WF ALPHA PREDICATE PAIR → ALPHA PREDICATE

∀ p 1 , p 2 : ALPHA PREDICATE |

( p 1 , p 2 ) ∈ WF ALPHA PREDICATE PAIR • p 1 ∧ P p 2 =( t B , t U )

Here, membership of ( p 1 , p 2 )to WF ALPHA PREDICATE PAIR encapsulates
an additional constraint for the compatibility of the universes of p 1 and p 2 .The
terms t B and t U respectively abbreviate the binding set and universe of the
result; their particular shape is not relevant here and for brevity is omitted.
Opposed to this, in HOL, the types of variables are part of their identity,
meaning that in a term like n ≥ 1 ∧ n = false (that may result from conjoining

Γ 1

≥

1andΓ 2 n = false ), we are effectively talking about two different

variables n distinguished by their types. We adopt a similar approach by moving
type information from the universe directly into the entities representing names,
which are now bindings of the following schema type.

n

VAR =[ name : STRING ; dashes : N ; subscript : SUBSCRIPT ; type : TYPE ]

The type STRING represents character sequences, and SUBSCRIPT is a free
type for representing a possible subscript. Importantly, the type component
records the type of the variable, and TYPE is equated with the non-empty sub-
sets of VALUE ,thatis, TYPE

P 1 VALUE . In comparison, in the previous
model, VAR only recorded a unique identifier (name), dashes, and a subscript.
This implies that the previous notion of 'universe' is subsumed by the con-
ventional notion of an alphabet, which now implicitly carry type information.
The encoding we obtain is in fact very similar to that originally developed by
Oliveira [12], but with the added benefit of concisely capturing type information.
The constraint bs

=

Bindings U u is notably redundant now in the definition of
ALPHA PREDICATE . We can also drop additional constraints in definitions
that require compatibility of types. Thus, the definition of

⊆

∧ P becomes