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

v neither impinges on f 's domain nor produces unsoundness if c ∈ dom f .This

is a property of the embedding of Z partial functions into HOL.
To illustrate the conceptual idea of the model, we consider, for example, the
set ALPHA PREDICATE . To capture undefinedness for functions encoding al-
phabetised predicate operators, we introduce the following set.

⊥ ALPHA PREDICATE = U \ ALPHA PREDICATE

It is simply the complement of ALPHA PREDICATE with respect to its corre-
sponding maximal type. In ProofPower-Z , acts as the carrier set of a generic

type which is inferred by the type checker, and which is always maximal. Here,
it would be the set

U

P (( P VAR ) × P ( VAR ↔ VALUE )).

For ∧ P , for example, we have the supplementary axiom below.

∀

p 1 , p 2 :

U |

( p 1 , p 2 )

∈ ∧ P •

p 1 ∧ P p 2 ∈⊥ ALPHA PREDICATE

dom( )

It does not affect (relative) consistency because none of the original definitions
impose any constraints on function applications outside their domains.
Finally, we can give a conservative definition for wd if applied to elements of
type ALPHA PREDICATE : wd p

∈⊥ ALPHA PREDICATE . The definition
provably satisfies the axiom for wd ( p 1 ∧ P

⇔ p

p 2 ) as it has been specified before,
and thereby establishes the correctness of the model, which itself is sound.
This model in a way simulates a treatment of undefinedness. It is correct if
the types are 'large enough' so that we can always find a witness that serves to
distinguish defined from undefined function applications.
There are cases where a collection of semantic types T 1 , T 2 , ... have the same
maximal type T max . For example, the semantic domain CIRCUS ACTION for
actions is a subset of ALPHA PREDICATE . In those cases, a single set ⊥ T is

defined as T max \ T i to ensure that ⊥ T is disjoint from all sets T i .Insuch

a situation, the union T i

needs to be a proper subset of T max , so that there

∈ ∀ • ∈ ⊥ T ∅

is some x T max for which i x T i . This implies that = ,whichis

crucial to prove that the model satisfies the axioms for wd .
Accordingly, there are functions in our encoding to which we cannot apply
wd . These are first the operators involving the

ProofPower-Z B type, which is

maximal. Since refinement is defined by a function with range B , we cannot

specify wd ( p 1 ). The impact of

this restriction is on provisos that involve refinements themselves. The extension
of our technique to handle such cases is left as future work.
Additionally, the domains of the functions that encode the various opera-
tors on values is VALUE , which is also maximal. This prevents us from spec-
ifying a well-definedness axiom, for example, for Eval ( b , e ), which evaluates
an expression under a binding and yields an element of VALUE . To handle
expressions, we axiomatise wd slightly differently; we define wd inductively
over the free type EXPRESSION that encodes the syntax of expressions. (Un-
like alphabetised predicates, they are embedded deeply.) We introduce a set
WT EXPRESSION containing the expressions that are well-defined, that is
{

p 2 ) ⇔ wd p 1 ∧ wd p 2 ∧ ( p 1 , p 2 ) ∈ dom (

e : EXPRESSION | wd e } . Since, the functions that encode Circus operators