any response

Let me try to field this one....

An Axiom is an unexplored statement.

The reason we have Axioms is to short-cut logic so that we don't consider all the various and unlikely scenerios.

The Semantics, or Content of an Axiom define how true it is.

It is assumed that an Axiom is true, (even if it is not) and logic preserves the truth or lack of truth of the statement.

Thus, verification of the accuracy of a system based on an Axiom, is heavily dependent on the Semantics of that statement. Essentially logic is an easy way to err with confidence, especially when the Axiom is oversimplified, Too complex, or just plain wrong.

Thanks smith, your argument makes sense

Gödel's theorema is still valid. Basically, any closed system will have one statement that can't be proved. That's its basic axioma. Applies outside mathematics as well, although not proven mathematically.

Axiomatic semantics is just one way of providing program semantics, in which program statements semantics is defined by using sequent-like rules. If I recall correctly the idea dates back to Floyd and was formalized by Hoare (receiver of a Turing award for his contributions to programming languages definition and semantics). These rules allow one to prove in a sequent calculus style the validity of a Hoare triple {Pre} Program {Post} (all the states that satisfy the precondition and for which the program terminates must satisfy the postcondition). Dijkstra showed how to translate these assertions to first-order logic formulas using the computation of the weakest precondition.

So, regarding verification, the relationship comes in two flavors: you can PROVE that a Hoare triple is valid by using Hoare's proof calculus (and this implies that the program is correct w.r.t. the provided pre and post conditions). Also, you can compute the weakest precondition and obtain a first-order formula (under the assumption that loops loop a bounded number of times) and use proof methods for first-order logic in order to verify the validity of Hoare triples. The latter approach is very much used in automated static analysis resorting to SMT solving or SAT solving, or related techniques.

I know the answer is not self-contained, but includes a few keywords for which abundant information is available on the web.

The book "The Science of Programming" by David Gries is a wonderful source for an introduction to this topic.

OK specialized knowledge is my face red!

Dear Graeme, your answer, although not exactly related to the problem, is correct. Greetings.

Here is a link to slides by Prof. Sifakis that explain the difference between axiomatic verification and other forms of verification.

http://risd.epfl.ch/files/content/sites/risd/files/sixseminars/Seminar3CorrectnessbyChecking%20-final.pdf

It is worth to study the whole presentation slide-by-slide.

dear Panagiotis Katsaros

thank you for PDF

i think the best answer can find to this PDF about communication between Algorithmic Verification and Axiomatic Verification

Very good presentation from Sofakis. Somebody who clearly can think cleanly.