4 ms·
Predicate logic is the base. Hoare logic rests on top of it to reason about the effect of commands in imperative code. Total correctness is used for Hoare logi
by helmut_brandl 11y ago
Predicate logic is the base. Hoare logic rests on top of it to reason about the effect of commands in imperative code.
Total correctness is used for Hoare logic. I.e. {Q} S {R} means that the program fragment S started in a state that satisfies Q will end up in finite steps in a state satisfying R.
For aliases I use something similar to separation logic. But I claim that it is much easier to use because it doesn't require to reason about the state of the heap. Some basic ideas can be found at https://softwareverificaton.wordpress.com/2012/06/03/abstraction-wins-an-approach-to-framing-and-mutability/ https://softwareverificaton.wordpress.com/2012/06/03/abstrac....
My current concept is much more refined and not yet published.
- mafribe 11y agoIf you use Hoare triples for total correctness, you can't reason about non-terminating programs. I recommend to use a Hoare logic for "generalised" correctness that enables you to reason about both, terminating and nonterminating programs. I would be interested in your ideas about aliasing. I don't think you can avoid the complications of separation logic or content quantification.
- helmut_brandl 11y agoFor non-terminating programs I use processes as described by Tony Hoare in "Communicating Sequential Processes". Procedures must always terminate in Albatross. If I have more documentation on aliasing, I can give you hint. Could you provide me some email address?