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

( ∧ P ): ALPHA PREDICATE × ALPHA PREDICATE → ...

∀ p 1 , p 2 : ALPHA PREDICATE • p 1 ∧ P p 2 =( t B , t A )

Most other definitions of our encoding can be simplified in a similar manner.
The notion of compatibility becomes obsolete since the common variables of
alphabetised predicates necessarily have the same type.
This enhancement also displayed benefits in terms of modularising proofs.
First, reasoning about alphabets (which are sets) is logically simpler than rea-
soning about universes (which are functions). Secondly, it is now possible to
introduce a notion of well-typed expressions independently of the universe con-
text; this makes provisos related to evaluation of expressions simpler.
We, however, still have many provisos like p ∈ ALPHA PREDICATE or

p ∈ CIRCUS ACTIONS . The following section explains how we deal with them.

3.2 A Semantic Formalisation of Well-Formedness

Our approach to capture well-formedness at the semantic level gives us the same
benefits as a syntactic characterisation of well-formedness in a deep embedding,
and importantly does not compromise soundness. To formalise well-formedness,
we introduce a generic HOL function wd of type a

BOOL where a is a type
variable. (Hereafter we use the term 'well-defined' in favour of 'well-formed'.)
Initially we do not specify any properties of wd , but for each semantic operator
op we add an axiomatic constraint of the following form.

→

wd ( op ( x 1 ,..., x n ))

⇔

wd x 1 ∧

... ∧

wd x n ∧ ( x 1 ,..., x n )

∈

dom op

The proposition wd ( op ( x 1 ,..., x n )) entails that op is applied in its domain,
and that all arguments are well-defined. Domain membership enables us to
extract properties of the arguments; for instance wd ( p 1 ∧ P

p 2 ) implies that

p 1 ∈

ALPHA PREDICATE . Moreover, for complex program terms, the prop-
erty of well-defined arguments allows us to extract well-definedness of any sub-
term. For example, wd ( p 1 ∧ P ( p 2 ∧ P p 3 )) implies wd p 1 , wd p 2 and wd p 3.

A potential risk with this approach is due to the definition of wd not being
obviously conservative. Generally in logic, conservative extensions maintain con-
sistency of the extended theory, and in many case this can be established by the
mere shape of the defining axiom. What we are doing, however, in defining wd
is in fact treating some Z function application op ( x 1 ,..., x n ) as if it revealed in-
formation whether the function was applied in its domain. It is not immediately
evident if and under what conditions such a treatment is sound.
To prove consistency, we provide a model which fulfils the defining axioms. The
essence of our model is the identification of values outside the domain and range
of each operator with undefinedness, and axioms that constrain applications of
operators outside their domains to be closed under this set. This is possible
because the underlying HOL logic is based on total functions, and therefore any
term denotes a value. Specifically, f ( x ) denotes a value even when x ∈ dom f ,

and constraining this value by an axiom such as f ( c )= v for particular c and