Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFifty years of Hoares Logic
175
0
0.0
(
0
)
Added by
Krzysztof R. Apt
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present a history of Hoares logic.
rate research
Read More
Hoares logic is an axiomatic system of proving programs correct, which has been extended to be a separation logic to reason about mutable heap structure. We develop the most fundamental logical structure of strongest postcondition of Hoares logic in Peanos arithmetic $PA$. Let $pin L$ and $S$ be any while-program. The arithmetical definability of $textbf{N}$-computable function $f_S^{textbf{N}}$ leads to separate $S$ from $SP(p,S)$, which defines the strongest postcondition of $p$ and $S$ over $textbf{N}$, achieving an equivalent but more meaningful form in $PA$. From the reduction of Hoares logic to PA, together with well-defined underlying semantics, it follows that Hoares logic is sound and complete relative to the theory of $PA$, which is different from the relative completeness in the sense of Cook. Finally, we discuss two ways to extend computability from the standard structure to nonstandard models of $PA$.
We provide a sound and relatively complete Hoare-like proof system for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism, and in which the correctness proofs are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no such proof system has been proposed in the literature.
The story told in this autobiographical perspective begins fifty years ago at the 1967 Gordon Research Conference on the Physics and Chemistry of Liquids. It traces developments in liquid-state science from that time, including contributions from the author, and especially in the study of liquid water. It emphasizes the importance of fluctuations, and the challenges of far-from-equilibrium phenomena.
This paper is concerned with the first-order paraconsistent logic LPQ$^{supset,mathsf{F}}$. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. For no logic that is essentially the same as LPQ$^{supset,mathsf{F}}$, a natural deduction proof system is currently available in the literature. The given embedding provides both a classical-logic explanation of this logic and a logical justification of its proof system. The major properties of LPQ$^{supset,mathsf{F}}$ are also treated.
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirqs tutorial on the Variational Quantum Algorithm (VQA).
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
