Floyd–Hoare logic
en.wikipedia.org
en.wikipedia.org
I've been thinking about this with functions, and trying to think of a way to make a programming language have support for a proof checker for this sort of thing built in, with functions having pre and postconditions, and function bodies that prove the postcondition is true after the function is run, given that the precondition was true before it was run, but I've encountered a problem when one allows first class functions.
If one allows first class functions, it seems that it would allow one to make tricks like "if this statement is true, 2+2=5". I'm not sure how to get around it.
It's possible that if one actually tried what I am thinking would be the problem, the preprocessor-thing (the thing that validates all the proofs before the program is actually run as a program) might just get into an infinite loop (through infinite recursion). But it doesn't look like that would necessarily happen.
And I'm not sure what thing in what I've written should be something that the proof validator should accept, but it certainly does not seem like the proof validator should accept all of it (because it can be used to "prove" anything that can be expressed in the language)
Your problem is, I think, assuming programs have correctness as an intrinsic property. This is not so. Programs can only be correct with respect to something - some idea born in a human mind, transcribed into something the checker understands (here, pre- and post-conditions). If the human mind wants 2+2 to equal 5 in their program, all power to them - they must only ensure this does not cause inconsistency.
Getting Started with Dafny: A Guide
1. undefined
2. undefined
3. undefined
...If you're not familiar with the idea of dependent types, it's definitely worth learning about them (and Coq is a good place to start) because they formalize the idea of arbitrary functions at the type level by letting types depend on values, giving you the ability to verify whatever invariants you like. A good place to start would be Benjamin Pierce's free Software Foundations[2] book.
There's a really rich theory here with a lot of both theoretical and practical problems worked out but, at the same time, lots of room to develop new ideas and approaches if this is something you're interested in.
[1]: http://ynot.cs.harvard.edu/
[2]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
I'm not going to get this right because I haven't even thought it out to my own satisfaction, but the fundamental difference seems to me to be that the those things treat a program as a mathematical object in itself, which is one of the reasons they focus on functional languages and immutability.
Floyd-Hoare treats the program as a text; it assigns states to the spaces between statements. As a result, it's pretty darn happy with imperative programming, although it has its own limits.
(As an aside (Did I mention that I once worked in the same building as Dijkstra, although I never took a class from him.), I find it very amusing that the article has the sentence "There are rules for concurrency, procedures, jumps, and pointers." although neither it nor the linked "Branch" article actually describe Knuth's revelation of Hoare's axioms for goto.)
Do you care to opine? :-)
Denotational semantics are horrible in my opinion, but I really like operational semantics (especially structural operational semantics and natural semantics), they still consider a program as a single mathematical object, but like Hoare logic it also tracks the state before and after each statement. It's really easy to work to with (just apply rules), but sadly it's a bit less powerful than Hoare logic, as you can't infer things that hold in general, you can only reason about specific begin states.
I see the point of semantics as capturing what programs mean. Denotational semantics does this in the most direct way, by giving me a mapping from programs to some abstract domain I can reason about and manipulate. It's literally a function from program to meaning.
It exposes a simple and natural model of my program—or, in the case of imperative programming, perhaps not so simple. As a facetious example, what should the program "1 + 1" mean? Adding two numbers seems like the most natural choice. But this can actually scale up quite far, producing simple models even for complex behaviors[1] as long as the language and libraries are designed with some taste.
Having simple denotational semantics captures exactly what it means for a language to be truly declarative, where we can think about what the program means and not how it happens to be executed.
Operational semantics is the next most direct option. It captures the meaning of a program by how it gets executed. Not quite declarative, but still reasonably easy to follow.
Axiomatic semantics, on the other hand, are really indirect. I mean, yes, I can see how you can capture a program's whole meaning by how preconditions are transformed throughout, but that's pretty far from what I think a program means. It's certainly useful and good for answering some very specific questions about a program's behavior, but it feels like a really unsatisfying answer to the broader question of semantics: what does it all mean?
[1]: A great example of how it scales to domains that are normally incredibly difficult to work with is functional reactive programming (FRP), which has a simple denotational model for working with time-varying values (ie reactive code). Unfortunately, as is too-often the case with nice abstractions, it has been hard to implement in general without compromises—but the nice thing is that we can know exactly what the compromises are by comparing the more complicated semantics of those libraries with the simple ones that we'd really like.
It uses separation logic which is an extension of Hoare logic for programs that manipulate the heap.
Furthermore, it is expensive to do: you need people with a strong understanding of mathematics/computer science, it is time intensive, and for most applications, just writing a program is good enough. But, to be honest, that goes for most formal methods. Well, unless they're completely automated, of course.