Information Technology Reference
In-Depth Information
parallel programs instead of sequential programs. This distinguishes our method from classical meth-
ods for program synthesis, such as those studied in type theory (Martin-Lof, 1980; Aarts et. al., 1992),
algebraic specification (Ehrig & Mahr, 1990), program transformation (Bauer et. al., 1985), deductive
synthesis (Manna & Waldinger, 1992; Traugott, 1989), term rewriting system (Klop, 1990; Meseguer &
Winkler, 1991; Meseguer, 1992), and other methods in automatic software engineering. Comparing to
automatic construction of sequential programs, the construction of parallel programs is a much harder
issue, because there is not a unified computation model for parallelism and concurrency, and details of
parallel architectures have to be considered when efficiency of the programs is to be improved (Paige
& Watcher, 1993). This method is based on the original first-order Gamma language, which is a single
module language. In this paper, we exploit this method on λ-Calculus, which is a higher-order language
fit for describing complex systems such as MAS.
Logical Speci.cation
In general, we shall be dealing with specifications of the form:
f
(
a
) ⇐ find
z
such that
Q
(
a
,
z
)
where
Q
[
a
,
z
] is a sentence of the background theory. Function
f
should be synthesized in a procedure
of theorem proving. The theorem corresponding to this specification is
∀
a
:
T
a
.∃
z
:
T
z
.
Q
(
a
,
z
)
In other words, for every input
a
of type
T
a
, there exists an output
z
of type
T
z
that satisfies the input-
output relation
Q
[
a
,
z
]. We assume there is a theory
TH
composed of
• Axioms and theorems on type
T
a
and
T
z
;
• Assertions about constrains on input
a
.
Theory
TH
can be used as facts in program construction. So the logic specification is:
spec
≡ ∀
a
:
T
a
. (
TH
→ ∃
z
:
T
z
.
Q
(
a
,
z
))
And we define
goal
≡ ∃
z
:
T
z
.
Q
(
a
,
z
)
In the following sections, we call
a input parameter
.
For example, the program verifying Goldbach Conjecture (Richstein, 2001) can be specified as
spec
≡
∀
n
:
N
.(
TH →
∃
m
,
k
:
N
.(
prime
(
m
) ∧
prime
(
k
) ∧
n
=
m
+
k
))
where
N
is the type of natural numbers;
Search WWH ::
Custom Search