Abstract: An important issue in the formal methods community
is the degree to
which mathematical sophistication and theorem proving skills should
be
needed to apply a formal method in software development. A fundamental
assumption in this talk is that many of the analyses made possible
by
formal methods research do not require mathematical sophistication
and
theorem proving skills. I will also argue that more ``practical" formal
methods are needed, i.e., methods that have a solid mathematical
foundation but do not require advanced mathematical training. Two
critical attributes of a "practical" formal method are 1) a
user-friendly notation for specifying the required system behavior
and
2) a set of tools that detect many classes of errors automatically
and provide feedback useful in error correction. Examples of
additional research (e.g., automatic abstraction methods and automatic
generation of invariants) that can help make current formal methods
more useful in practical software development are proposed. Also
suggested are tool features that would encourage more widespread use
of formal methods by practitioners. To illustrate these ideas, I will
present examples based on the SCR (Software Cost Reduction)
requirements method and describe our experience applying the SCR
method to a number of practical systems.
Abstract: The ever-increasing software content in future products,
the seemingly
uncontrolled complexity of current development and implementation practices,
the largely unrealized promise of software reuse, and the consequent
effects
on timely delivery of reliable and competitive products are all compelling
reasons for pre-emptive action to explore and methodically adopt innovative
approaches that will gradually improve productivity of software based
products by 100X over the next few years. Motivated by the obvious
successes
in the hardware industry, encouraged by recent trends in software component
technology, and inspired by the impressive advances in applied constraint
satisfaction, the proposed approach takes the form of an optimal control
system specifically structured to support an adaptively improving software
product development process by making judicious use of prefabricated
commodity objects and guided by intelligent automation to jointly achieve
excellence in technology and success in the marketplace.
Abstract: One major drawback of logic programming, particularly
Prolog, =
is the lack of mechanisms for structuring knowledge (i.e. program =
clauses). This makes programming-in-the-large a difficult task even
=
using the module system. Various attempts were made to extend the logic
=
programming paradigm with object oriented features. In this paper we
=
introduce LOOP, another object oriented extension of Prolog which =
provides object oriented features very similar to those found in =
imperative object oriented languages (e.g. C++, Java), in a very simple
=
and straightforward fashion. In LOOP an object is considered to be
a =
persistent mutable Prolog term, and therefore, objects can be =
manipulated in a very similar way as classical logic terms. We believe
=
that the unique set of LOOP features makes it very suitable for rapid
=
prototyping and programming-in-the-large.
Keywords: logic programming, Prolog, object oriented programming, rapid
=
prototyping, programming-in-the-large.
Abstract: Most program development methods rely on a combination
of
programming and logical notations. Correctness is verified using
refinement laws which often have logical side conditions. Checking
these conditions involves a separate proof, breaking up the linear
flow of the program derivation. This paper explores a variant of
the refinement calculus in which only logical notation is used and
the program under development is inferred from formulas which are,
in effect, the verification conditions that would arise in a
traditional derivation. It is preferable that these are verified
first, in which case they should be called verified conditions. A
polynomial algorithm exists for extracting the refinement argument,
and hence the implementation, from these conditions. A prototype
code generation system has been implemented in Prolog. The benefits
and weaknesses of the approach are compared to those of more
conventional refinement calculi.
Abstract : This paper proposes an approach to the evaluation
of B formal specification
s in Set Constraint Logic Programming. For the evaluation of the specifications,
invariant and the pre-conditions with substitution mechanism must be
verified
and the graph of reachable states of the specification assessed.
This paper presents a system for constraint resolution to B formal specifications.
This solver is described in terms of constraint domains, consistence
verification
and constraint propagation. The constrained state is defined. It was
used to
propagate the indeterminism of the specifications and reduce the number
of
states in a reachable graph.
The graph exploration was used in animation of specifications. We illustrate
this
approach by comparing the constrained states graph exploration with
the valued
one in a simple example: Process scheduler.
Key words : B Method, Evaluation of specifications, Animation, CLP, CSP, Set constraints
Abstract: In this paper we propose a new approach to implement
web services
based on the Common Gateway Interface (CGI). Since we use the
multi-paradigm declarative language Curry as an implementation
language, many of the drawbacks and pitfalls of traditional CGI
programming can be avoided. For instance, the syntactical details of
HTML and passing values with CGI are hidden by a wrapper that executes
abstract HTML forms by translating them into concrete HTML code. This
leads to a high-level approach to server side web service programming
where notions like event handlers, state variables and control of
interactions are available. Thanks to the use of a functional logic
language, we can structure our approach as an embedded domain specific
language where the functional and logic programming features of the
host language are exploited to abstract from details and frequent
errors in standard CGI programming.
Abstract: To date Logic Programming has not made any impact on
Software
Engineering. As Software Engineering moves on from objects to
components, will Logic Programming be simply forgotten forever? In
this
position paper, I will argue that the answer could be and should be,
perhaps
surprisingly, negative.
Abstract: Declarative programming, with its mathematical
underpinning, was aimed to simplify rigorous reasoning
about programs. For functional programs, an algebraic
calculus of relations has previously been applied to
optimisation problems to derive efficient greedy or
dynamic programs from the corresponding inefficient but
obviously correct specifications. Here we argue that this
approach is natural also in the logic programming setting.
Abstract: In this paper we investigate how logic programming
technology
can aid software development. Two approaches are discussed. In the
first approach, given a program written in a traditional language
(e.g., C), an equivalent logic program is automatically obtained.
This equivalent logic program serves as a high level abstraction
of the original program and can be put to a number of uses including
debugging and code generation. The second approach is centered around
domain specific languages. Given a task for which a software system
is
to be developed, a high-level domain specific language is first designed.
Domain experts can use this DSL for writing programs at their level
of abstraction. Logic programming provides a framework in which programs
written in this DSL can be interpreted, compiled, debugged,
and profiled.
Abstract: The CASE tool AUTOFOCUS allows for modeling and validating
reactive systems on the basis of a simple, clearly defined formal semantics.
It is shown how executable code for common CLP languages can be generated
automatically. Aplicaitons include simulation for rapid prototyping
and debugging as well as semi-automatic generation of test-sequences.