Questions tagged [program-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
18
votes
3answers
463 views

Frame rule as a change-preserver?

A frame rule, like the one given below, captures the idea that, given a program c with precondition p that holds before it runs ...
8
votes
2answers
342 views

Original Hoare Logic termination paper

I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by ...
10
votes
2answers
789 views

Ownership types and Separation Logic

Ownership types and Separation Logic seem to have similar goals, control over ownership and aliasing. Perhaps, I should also add: the ability to write modular specifications. What is known about the ...
14
votes
3answers
540 views

How hard is it to reduce termination to partial correctness?

If you are familiar with program verification you are likely to prefer reading the Question before the Background. If you are not familiar with program verification then you may still be able to ...