[TYPES] Variants and [Park or Scott] fixpoint Induction

[Tadeusz Litak]

On 15.06.19 12:23, Sergey Goncharov wrote:
>
> in Hoare logic we essentially have a global choice between weakest 
> preconditions for total correctness and weakest (liberal) 
> preconditions for partial correctness. Computationally the former are 
> completely different kind of properties (co-r.e.) in comparison to the 
> latter (r.e.) in the arithmetical hierarchy. 


This seems to depend on the programming language you are talking about. 
For example, this is what Clarke, German and Halpern write in the 
conclusion of their POPL 1982 paper "On effective axiomatizations of 
Hoare logics":


> This leads us to our last point: the relationship between partial 
> correctness and termination,
> and our ability to find good axiom systems for complicated programming 
> languages. One conclusion we can draw is that under the assumption 
> that the halting problem is decidable for finite interpretations, 
> partial correctness and termination seem to have essentially the same 
> complexity. However, for more complicated deterministic programming 
> languages such as those discussed in [Cl76/79] which do not have a 
> decidable halting problem for finite interpretations,  termination 
> assertions, and hence total correctness assertions, are effectively 
> axiomatizable, while partial correctness assertions are not. This 
> suggests the use of a total correctness proof system which, unlike 
> most currently available, does not require the establishment of 
> partial correctness as an essential first step.