Summary
Summary Automatic Programming Artificial Intelligence
- Module
- Artificial Intelligence
- Institution
- Oxford University (OX)
This pdf will help you to understand the concept of Automatic Programming of artificial intelligence
[Show more]
Seller
Follow
Content preview
J . Symbolic Computation (1985) 1, 119-142Automatic Programming :
A Tutorial on Formal Methodologies
ALAN W . BIERMANN
Department of Computer Science,
Duke University, Durham, North Carolina 27706, U .S.A .
(Received 4 March 1985)
Ten methodologies for automatic program construction are presented, discussed and
compared . Some of the techniques generate code from formal input-output specifications
while others work from examples of the target behaviour or from natural language input .
1 . Introduction
Computer programming is the process of translating a variety of vague and fragmentary
pieces of information about a task into an efficient machine executable program for doing
that task . Automatic computer programming or automatic programming occurs whenever a
machine aids in this process .
The amount of automatic programming that is occurring is a variable quantity that
depends on how much aid the human is given . There are a number of dimensions on
which the level of help can be measured including the level of the language used by the
human, the amount of informality allowed, the degree to which the system is told what to
do rather than how to do it, and the efficiency of the resulting code . Thus we usually say
that there is a higher degree of automatic programming whenever a higher level language
is used, less precision is required of the human, the input instructions are more declarative
and less procedural, and the quality of the object code is better .
The technologies of automatic programming thus include the fields that help move the
programming experience along any of these dimensions : algorithm synthesis,
programming language research, compiler theory, human factors, and others . This paper
will concentrate on only the first of these topics, formal methodologies for the automatic
construction of algorithms from fragmentary information .
The formal methodologies - have been separated into two categories, synthesis from
formal specifications and synthesis from examples . In the former case, it is assumed a
specification is given for the target program with adequate domain information so that
the target program can be derived in a series of logical steps . In the later case, behavioural
This material is based on work supported by the Air Force Office of Scientific Research, Air Force Systems
Command, USAF under Grant 81-0221 and the U .S. Army Research Office under Grant
DAAG-29-84-K-0072 . '
t The formal methodologies that transform specifications, domain information and behavioural examples
into programs operate on symbolic objects (logical formulae and programs) and aim at total or partial
automatisation of this transformation process . Also, most of these methodologies are intimately connected with
automatic theorem proving . Hence, automatic programming should be viewed in the context of symbolic
computation as defined in the editorial of this journal .
0747-7171/85/020119+24 $03 .00/0 © 1985 Academic Press Inc . (London) Ltd .
5
,1 20 Alan W . Biermann
examples are given for the desired program, and it is inferred by a series of generalisation
steps .
After completing the coverage of these formal methodologies, a short section mentions
some work on the generation of programs from natural language input using artificial
intelligence knowledge based systems .
The various synthesis methodologies will be described by illustrating their operation on
a single programming problem . In all cases, many details have been omitted or modified
from the original sources to maintain brevity and readability . The reader is always
encouraged to return to the referenced papers for more complete coverage .
2 . Information Sources
The target program in a programming environment must be derived from basic
information about the desired behaviour . Some of this information is furnished by the
4i.rman user and some may be general domain knowledge . In all cases, enough
information must be available to specify the target program .
However, the "structural distance" between the source information and the target may
vary greatly . In some cases, the form of the axiomatic information may be quite close to
that of the generated code, in which case we say that little automatic programming has
occurred . In the extreme case, the user gives code in a compiled language that can be
directly translated into the target language . In a less severe case, the user needs to specify
axioms in a relatively exacting form, and the synthesiser performs only modest
translations to assemble the target . In the most impressive cases, the source of
information may be extremely random and fragmentary in nature leaving the synthesiser
to discover essentially all of the structure required to do the computation .
For the sake of concreteness, we will study synthesis methodologies as they construct a
program to remove the nonatomic entries from a list . Thus the desired behaviour
transforms the input list (A (B) C) to (A C) . If the input list has length zero, the output list
is this same list, i .e . nil yields nil . The process of generating this program illustrates the
construction of both a loop and a nested branch .
Relatively standard notations will be used in this paper If x = (A (B) C) then car (x) will
be a function that finds the first entry on the list, A . The function cdr (x) will return list x
with the first entry removed, ((B) C) in this example . The cons (u, v) operator will add its
first argument u to the front of its second argument, list v . Thus cons (x, x) will yield
((A (B) C) A (B) C) . The symbol atom is a predicate which yields true if its argument is an
atomic unit or list of length zero . Thus atom ((A (B) C)) is FALSE and atom (A) is TRUE.
The function length will give the length of a list . Thus length ((A (B) C)) is 3 .
In specifying the example problem given above, several key facts need to be included .
Thus it will be necessary to give the fact that input nil is to yield output nil . This will be
known as fact F1 in later discussions . It may be written as
if x = nil then f(x) = nil (F1)
where f is the name of the target program . But some synthesis methodologies will require
other notations . For example, the notation R(x, z) will denote the target relationship
between the input x and output z . So the nil case is specified as R(nil, nil) or as
R(x, nil) =:~, TRUE if x = nil. The => symbol can be read as "may be replaced by" .
If the input list x is not nil, its associated output z must also be specified . Considering
the output list as a set, one can write f(x) = z where
, Automatic Programming : A Tutorial on Formal Methodologies 121
for all u[member(u, z) <-> (member(u, x) and atom (u))] .
Another way of encoding this information is to say that
If not (x = nil) and not (atom (car(x))) and R(cdr(x), u)
then R(x, u) . TRUE (F2)
and
if not (x = nil) and atom (car(x)) and R(cdr(x), u)
then R(x, cons(car(x), u)) => TRUE (F3)
All of these forms will be used in the examples below .
The careful reader may object to synthesising programs from information as specific as
the axioms given above . They are in some sense already executable in their current form
and are thus programs as they stand . For example, the latter forms are almost identical to
the following PROLOG program .
R(nil, nil) <-
R(x, y) <- R(cdr(x), y), not(atom(car(x))),
not(atom(x))
R(x, cons(car(x), u)) <- R(cdr(x), u),
atom(car(x)), not(atom(x))
Thus one can compute f(x) = z by proving the theorem R(x, z) on a PROLOG system .
However, the synthesised programs given below are deterministic and thus compute much
more efficiently than one can expect to execute specifications . The theorems implicit to the
programs are already proved and there is no uncertainty related to their execution . The
interpretation of specifications is dependent on the nature of the interpreter, the ordering
of the axions, and other extraneous factors . The fact that specifications can be executed
does not necessarily obviate the need for generating deterministic code .
3. Synthesis from Formal Specifications
Many methodologies have been developed in recent years for the generation of
programs from specifications . Five of them will be described here : the strategical approach
of Bibel & Hornig (1984) which has been embedded in the LOPS system, the divide and
conquer methodology of Smith (1985), the transformational technique as developed by
Broy (1983), the deductive sequent method of Manna & Waldinger (1980), and the
synthesis from equational specifications as described by Prywes et al . (1979) .
3 .1 . A STRATEGICAL APPROACH
Bibel & Hornig (1984) have constructed the logical program synthesis system LOPS
which has a variety of facilities for acquiring specification information, manipulating
domain knowledge, proposing critical theorems and proving them, and constructing code .
We will follow their methodology as it solves the synthesis problem posed above . The
system searches for relationships between the input and output and attempts to guess a
portion of the input which can be selected out to begin computation of the output . If this
is successful, it then attempts to find a recurrence of the original specification in the
reduced form of the problem with part of the input already processed . If the recurrence
The benefits of buying summaries with Stuvia:
Guaranteed quality through customer reviews
Stuvia customers have reviewed more than 700,000 summaries. This how you know that you are buying the best documents.
Quick and easy check-out
You can quickly pay through credit card for the summaries. There is no membership needed.
Focus on what matters
Your fellow students write the study notes themselves, which is why the documents are always reliable and up-to-date. This ensures you quickly get to the core!
Frequently asked questions
What do I get when I buy this document?
You get a PDF, available immediately after your purchase. The purchased document is accessible anytime, anywhere and indefinitely through your profile.
Satisfaction guarantee: how does it work?
Our satisfaction guarantee ensures that you always find a study document that suits you well. You fill out a form, and our customer service team takes care of the rest.
Who am I buying these notes from?
Stuvia is a marketplace, so you are not buying this document from us, but from seller hamzasuleman. Stuvia facilitates payment to the seller.
Will I be stuck with a subscription?
No, you only buy these notes for £2.48. You're not tied to anything after your purchase.
Can Stuvia be trusted?
4.6 stars on Google & Trustpilot (+1000 reviews)
48298 documents were sold in the last 30 days
Founded in 2010, the go-to place to buy revision notes and other study material for 15 years now