Abstracts for publications in nonstandard dynamic logic of Andréka, H. and Németi, I.
[ANBSL78]
The Floyd-Hoare method for proving program correctness is
complete wrt the so-called continuous-traces semantics. It is not complete wrt the
standard-traces semantics of programs. Full proofs are contained in [ANSMFCS79].
[ANSBSL79]
Thm.1 states a strong incompleteness property for program
correctness statements with the standard semantics: there is no recursive set
containing the “we must prove these program correctness statements” and
contained in the standard -valid program correctness statements. Thm.2. states
that the reason for this incompleteness is in the definition of standard
semantics for program correctness statements: this standard semantics is not
stable in Zermelo-Fraenkel Set Theory. These
theorems justify the Henkin-type semantics for dynamic logic introduced
in other papers. This paper is an abstract for the first part of [ANSMFCS79].
[ANSMFCS79]
Thm.1 states a strong incompleteness property for program correctness
statements with the standard semantics: there is no recursive set containing
the “we must prove these program correctness statements” and contained in the
standard -valid program correctness statements. Thm.2. states that the reason
for this incompleteness is in the definition of standard semantics for program
correctness statements: this standard semantics is not stable in
Zermelo-Fraenkel Set Theory. These
theorems justify the Henkin-type semantics for dynamic logic introduced
in the second part of the paper, for which Thm.3 states strong completeness.
[ANSMFCS81]
An explicit characterization of the information content of the
Floyd programverification method is given, as follows. A run (sequence of intensions of the registers) in
perhaps nonstandard time of a program is called continuous if it satisfies
induction over all possible dynamic logic formulas containing one free time
variable. Thm.1: Assume that T is a
theory about data containing the Peano’s Axioms. A program p is
correct for output formula psi wrt each
continuous runs in each model of T if and only if p can
be proved correct wrt psi by the Floyd inductive assertion method. Detailed
proof is given.
[NKoz82]
NDL , and a
lattice of program verifying methods are introduced. In this lattice,
comparison of theories in NDL are based on their strengths for proving partial
correctness of programs. Figure 2
contains many statements about this lattice. Thm.6: Ia+Ts is strictly weaker
than Ia+To. Intuitively: When using full
induction Ia over time, it does matter
whether we can compare time instances by “later than” relation, or we just have
successor on time. (Used together with quantifier-free induction over time in
place of full induction, this does not
matter.) Thm.6 is proved in detail with
figures.
[ANSTCS82]
Part I:
Nonstandard Dynamic Logic (NDL) is introduced, by replacing standard semantics
of First-order Dynamic Logic (FoDL) with an explicit time semantics. NDL is then proved to be strongly complete
wrt a proof concept ⱵN
(Thm.2, detailed proof, translating NDL into FOL). It is known that FoDL
is rather wild, e.g., its validities are not recursively enumerable, hence the
move to explicit time semantics was necessary to obtain the above completeness
theorem (analogous to Henkin’s Nonstandard Second-order Logic). The proof
system ⱵN is a new rather strong method for proving
properties of programs (see Part II of the paper).
Part
II: NDL, introduced in Part I, is shown
to be useful for reasoning about programs and for characterizing the information contents of known program
proving methods. First, natural properties of programs are proved under natural
axioms about time. (Thm.3,4) Termination of the ``count-down program” is proved
by using the order axioms on time, induction on data, and comprehension on
intensions (Thm.7). The Naur-Floyd-Hoare
inductive assertions method for proving correctness of programs ⱵF
is introduced (section 6). Thm.9 is a semantic characterization, in
terms of statements in NDL, of the information implicitly contained in the
Floyd-method. This information content is time-induction over quantifier-free
formulas . If in addition we can reason about ordering in time, our
program-proving abililty does not increase, we do not go beyond the power of
Floyd’s method. But if we can perform addition on time, or if we can quantify
over time points in the induction, our reasoning ability is beyond the power of
Floyd’s method. Note that quantifying over time is roughly the same as using
time-modalities. However, if our theory for the data contains the Peano axioms,
full induction over time does not lend morereasoning power than the Floyd
method (Thm.11). The proof concept ⱵN is strictly stronger than Floyd’s method
(Thm.10).
A slightly
updated version with detailed proofs, some new material on the lattice of
program verification methods, and plenty of illustrations is [ANSComp81].
[ASalw83]
The main
result is that induction over formulas containing a single universal quantifier
of sort time is already strictly stronger than Floyd’s method, for proving
partial correctness of programs (Thm.2). It was known that Floyd’s method is
equivalent to induction over formulas not containing quantifiers of sort time
([ANSTCS82], Thm.9). The case for induction over formulas containing a single
existential quantifier is left open. This paper is a continuation of [NKoz82].
[NSalw83]
The question
“exactly which programs are provable by the Floyd-Hoare inductive assertions
method” is investigated. Concrete examples of simple nonstandard runs of
programs are constructively defined and illustrated. The emphasis is on
simplicity, with the aim to make nonstandard runs and nonstandard models less
esoteric, less imaginary, easy to draw, easy to touch. It is demonstrated how ultraproducts can be
used to test applicability of Floyd’s method in concrete situations.
[ANSMFCS89]
This is a
shorter, abstract version of [ANSTCS91].
[ANSComp81]
This is an
updated version of [ANSTCS82] with detailed proofs, some new material on the
lattice of program verification methods, and plenty of illustrations.