Information Technology Reference
In-Depth Information
also discuss those alterations here. We evaluate our new technique by encoding
tactics that perform part of a refinement strategy for control laws [3].
Section 2 introduces the relevant preliminary material: core aspects of our
semantic embedding of
Circus
ArcAngel C
, and its implementation. Section 3
explains our solution to managing well-definedness, and Section 4 discusses the
accompanying extensions to the
,
ArcAngel C
implementation. Section 5 reports
on a case study, and in Section 6 we present our conclusions and future work.
2 Preliminaries
In this section, we first present relevant details of our mechanisation of
.
The mathematical notation we use is standard Z [16], but the ideas in Section 3
and Section 4 also exploit the higher-order support afforded by ProofPower being
based on HOL. We secondly briefly introduce ArcAngel C
Circus
and its implementation.
2.1 Mechanisation of
Circus
Circus
The mechanisation of
is based on its denotational semantic model [12],
which is formulated in terms of the Unifying Theories of Programming (UTP) [6].
The UTP is a general framework in which the semantics of a variety of modelling
and programming languages can be uniformly expressed. It is founded on a
relational calculus like Tarski's, but presented in a predicative style.
In the UTP, relations represent computational behaviours. To encode them,
we use alphabetised predicates , which are predicates equipped with an alphabet
of variables. The predicate x
x
1, for example, encodes the
computation that either increments or decrements the value of x ; its alphabet
includes x and x . We use undecorated names to denote initial observations of
the value of a variable, and dashed names to denote subsequent ones. In the
UTP theory for
= x +1
= x
, alphabetised predicates describe actions and processes.
In our mechanisation, an alphabetised predicate is a pair.
ALPHA PREDICATE = {bs : BINDINGS ; u : UNIVERSE | bs ⊆ Bindings U u}
Its first component is a set of bindings (records) describing the valuations of the
variables of the alphabet that render it true. The second component records the
types of the alphabet variables. BINDINGS is the type of all binding sets, and
UNIVERSE consists of all partial functions from VAR to TYPE ,where VAR
is the semantic domain for variables, and TYPE (
Circus
=
P 1 VALUE ) contains all
non-empty sets of values. The condition bs
Bindings U u effectively establishes
that the bindings of a predicate have to be well typed. (The function Bindings U
constructs the complete set of bindings according to a given typing universe.)
Alphabetised predicates are embedded shallowly in the mechanisation: we
characterise their semantics, but do not formalise the syntax of the UTP and
the
language. Instead we provide a collection of semantic functions that
correspond to the various syntactic constructs.
We define in [19] operators that provide the logical connectives, equality, sub-
stitution, including all
Circus
constructs, and importantly refinement. The latter
allows us to state that some (concrete) program P behaves according to its
Circus
 
Search WWH ::




Custom Search