Timeline for Program transformation as alternative for Hoare logic or temporal logic
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 29, 2011 at 21:13 | vote | accept | Lucas K. | ||
| Jul 21, 2011 at 6:42 | answer | added | Andrej Bauer | timeline score: 4 | |
| Jul 21, 2011 at 1:32 | answer | added | Vijay D | timeline score: 2 | |
| Jul 10, 2011 at 11:19 | comment | added | Lucas K. | @Andreas, I edited the question. If you wish, you can fully narrow it down in transforming a program in a FOL + PA expression. Using Hoare logic or transforming it in a FOL + PA expression, is quite a different approach (although at the end it might not be that different). The first approach you find in the standard books and in the Wikipedia, the second not. | |
| Jul 10, 2011 at 10:44 | history | edited | Lucas K. | CC BY-SA 3.0 |
Clarification.
|
| Jul 10, 2011 at 8:02 | comment | added | Neel Krishnaswami | As Andreas points out, the known techniques are hardly exhausted by Hoare and temporal logic! However, given the thrust of your question, I would suggest looking at "refinement calculus" (see the book of Beck and von Wright: amazon.com/dp/0387984178). The idea in it is to view both programs and specifications as predicate transformers, with programs being a realizable subclass of the predicate transformers. Back also maintains a bibliography at users.abo.fi/backrj/… | |
| Jul 10, 2011 at 1:32 | comment | added | Andreas Blass | What you describe, expressing programs in a logical formalism, is extremely broad and the associated literature is immense. You're more likely to get relevant answers if you give a narrower description of what you're interested in. For example, how does it differ from just "write programs in declarative languages"? How does it differ from denotational semantics of programming languages? For that matter, how does it differ from descriptive complexity theory? Each of these is a huge area, and you surely don't want references for all of them (and more). | |
| Jul 9, 2011 at 22:27 | history | asked | Lucas K. | CC BY-SA 3.0 |