Algorithmic Logic
its home page
Table of contents
- Definition per genus proximus et differentia specifica
- Goals of AL
- Structure of AL
- Applications
- specifications of algorithms, data structures and programming languages
- analysis of properties of programs (verification)
- axiomatic definition of programming languages
- Copyrights
- Readings
- What's new in AL?
- Invitation to projects
- the assistant in proving, more precisely ...
- an axiomatic specification of the Loglan'95 programming language...
-
- algorithmic logics
- are a kind of logics of programs, their components are:
a formalized algorithmic language and
a consequence operation defined by means of logical axioms and inference rules.
- logics of programs
- is a family of logics, the language of a logic of programs admits
programs as modalities.
Examples:
- calculus of Floyd (descriptions of flowdiagrams)[1967],
- calculus (Hoare) of partial correctness formulas [1969],
- algorithmic logic [1969-1994],
- calculus of weakest preconditions (Dijkstra)[1974],
- dynamic logic [1976], etc.
- an algorithmic language
-
is the smallest language which contains both the set of programs and the set of first order formulas and which is closed under the formation rule:
if P is a program and f is a formula then the expression Pf is an algorithmic formula. The set of algorithmic formulas admits the usual formation rules: disjunction, conjunction, negation, implication, quantification.
- the study of semantic properties of computer programs. The role of AL
in computer science is similar to that of mathematical logic in mathematics.
AL studies those properties of programs whih are valid by virtue of their
syntactical structure, independently of any interpretation of functional and
relational symbols in programs. This leads to the discovery of algorithmic
tautologies and inference rules, thus enabling algorithmic reasoning.
Various programming constructs, one may say, various programming languages
lead to various logics. In one logic you can discuss the properties of
deterministic iterative programs, in another one may analyse the properties
of concurrent(hence non-deterministic) programs, in yet another ...
The theories based on AL are of interest for the study of abstract data types.
For example, an algorithmic theory of stacks is the theory determined by its
algorithmic language and the set specific axioms,
-
A recipe:
Take one programming language Lp and its semantics. Consider the
semantical phenomena of the executions of programs (like termination,
correctness, partial correctness, equivalence etc.). Add a first-order
language L1. Mix well, you will obtain an algorithmic language La.
Remark its capability to express the semantical properties of programs
(mentioned earlier).
What you need now is a handful of axioms and inference rules. Be careful.
Avoid inconsistency. Search for the completeness of your logic.
Now, you are ready to serve formal proofs
of semantical properties of programs and other theorems.
-
- specification of algorithms, data structures and programming languages
A program K is specified by a pair of formulae alpha and beta. The formula
of the form
alpha => K beta
is satisfied by a state of memory s iff either s does not satifies the
precondition alpha, or if program K transforms the initial state s into a
resulting state s' (i.e. no infinite loops, no fails either) and the state
s' satisfies the post-condition beta.
A set Z of formulae specifies a (family of) data structure(s) iff all formulas
are valid in the data structure belonging to the family and no data structure
outide the family satisfies all the formulae of the given set Z
- verification and more precisely analysis of properties of programs
One does it by proving the formulas that express the properties f programs
- axiomatic definition of programming languages
In a paper we we proved that the meanings of programming operators such as
assignment operator, composition of programs operator begin... end,
condititional instruction operator if ... then ... else ... fi operator,
iteration instruction operator while... do ... od are uniquely determined
by he fact that they satisfy the tautologies of algorithmic logic and that
they are conformant to the inference rules of AL.
In other papers we show that the primitive data types of programming languages
are axiomatizable and we study their algorihmic theories.
-
-
What to read?
-
We would like to announce two results of 1994.
In spite of the Tennenbaum's theorem
it is possible to
to construct a programmable and non-standard model for
the elementary theory of stacks.
The same remark applies as well to other specifications.
Theorem 1
Let S be the algebraic specification of stacks. There exists a programmed
module Stacks which correctly implements all the axioms mentioned in the specification S,
the module Stacks admits infinite popping of certain stacks.
WARNING. Be careful, it may be the case that a software module satisfies
all axioms of a given first-order specification, yet it may be pathological
one. The facts: a module fulfills the axioms and the module is programmable
do not necessarily means that the module has any value.
Theorem 2
Algorithmic theory of stacks of bounded capacity is the
complement of a recursively enumerable set.
Intuitively speaking this result gives an assuring answer to the question
'Can one do the research of properties of programs
using the calculus of AL? The nature of AL seem so complicated. Perhaps it would be better
to use another logic of programs.'
Quite unexpectedly the oponents of AL are confronted with
two facts:
- the dynamic logic has finitistic inference rules and
the highly undecidable set of axioms,
- the algorithmic logic has a number of omega-rules,
but the set of theorems of algorithmic theories of
practical interest is relatively low in the hierarchy of Kleene-Mostowski.
-
- the assistant in proving, more precisely ...
- an axiomatic specification of the Loglan'95 programming language...
Explanations of notions used
Algebraic specification of stacks:
The universe is a union of two sets S- for stacks and E- for elements.
Operations and predicates:
push: E x S -> S
pop: S -> S
top: S -> E
empty: S -> {true, false}
Axioms:
not empty(push(e,s))
s = pop(push(e, s))
e = top(push(e, s))
not empty(s) => s = push(top(s), pop(s))
Back
Tennenbaum's theorem
If M is a recursive(i.e. programmable) model of Peano's
axioms of arithmetic of natural numbers then it is isomorphic to the
standard model of natural numbers.Back
GM y AS 10:07 01/01/1995