Information Technology Reference
In-Depth Information
(abstract) specification
S
. Formally, this is expressed by
S
P
, and given the
mechanisation we can, by aid of a collection of refinement laws, prove whether
a given refinement holds. To automate this process, we have implemented a
bespoke tactic language
ArcAngel
C
; it is explained in the next section.
2.2
ArcAngelC
ArcAngel
C
programs from speci-
fications [10]. (Hereafter, we will use the word 'program' synonymously for both
specifications and programs.) A salient feature of
ArcAngel
C
is a tactic language for the derivation of
Circus
is first that it sup-
ports backtracking through angelic choice, namely from failure of tactic applica-
tions. This it inherits from its kin
Angel
[7], which is more generally concerned
with proving arbitrary goals. Secondly, it has a formal semantics that has been
specified in the Z notation, and permits the reasoning about tactics.
Basic literal tactics provided by the
ArcAngel
C
are
skip
,whichleavesthe
program unchanged,
fail
, which always fails, and
abort
, whose application is
not guaranteed to terminate. To apply refinement laws, the tactic
law
name
(
args
)
takes the name of the law and a list of arguments. Compound tactics may be
declared using the
Tact i c
name
(
args
)
=
body
end
construct.
We further have the binary tacticals
t
1
;
t
2
for sequence and
t
1
t
2
for al-
ternation. Sequence executes the tactics one after another, and alternation first
attempts to apply
t
1
, and if that fails, applies
t
2
. Other tactics are !
t
which
acts like a cut on the backtracking search of finding a successful path of tactic
execution, and
applies to
p
do
t
which guards the application of a tactic
t
by
successful matching of the program against a pattern
p
. Finally, recursive tactics
are supported via the fixed-point operator
μ
X
|
•
t
(
X
).
action or process construct, a set
of structural combinators is provided. They are boxed versions of the respective
Circus
To apply tactics to the operands of a
Circus
operators. For example, the combinator
t
1
t
2
applies to actions of the
form
a
1
a
2
. Its behaviour is to apply
t
1
to
a
1
and
t
2
to
a
2
. The application is
justified by the monotonicity of
Circus
operators with respect to refinement.
in
ProofPower
[18]. The fundamental design
of the implementation supports tactics as theorem-generating functions that ap-
ply to program expressions
A
and return lists of refinement theorems Γ
We have implemented
ArcAngel
C
B
.
The construction of refinement theorems is necessarily sound because of the LCF
approach that prevents invalid theorems from being derived. More specifically,
ProofPower-Z
uses the type system of the prover's implementation language (ML)
to differentiate between (unproved) conjecture and (proved) theorems.
A
3 Managing Well-Definedness
Most of the laws of our
semantic encoding specify well-definedness provisos
for their applicability. The provisos ensure that relational expressions, such as
p
1
Circus
p
2
, as well as operator applications, like
p
1
C
p
2
, are well-defined, that
is, the underlying semantic functions are applied inside their domain.
Search WWH ::
Custom Search