Statements of the panelists
made the following statements:
For correct programs, start with - empirical evidence - proofs are needed based on precise specifications, e.g. by
electrical circuit viewed as a function from input to output
inheritance hierarchies based on independently defined semantics
The problem which comes up is here complete vs. incomplete specification.
First, one needs a good design. Second, small tricks, which preserve equivalence in some sense (strong, unif., weak). Michael shows two examples:
a :- -b. s a :- not b.
-b :- not b. <===> -b :- not b.
:- a,b. add
:- -a,c. ===> :- b,c.
We miss function symbols.
Stefan Woltran 2005-08-22