اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدFifty years of Hoares Logic
175
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We present a history of Hoares logic.
قيم البحث
اقرأ أيضاً
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 linea
r 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 just
ification 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- a
nd 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).
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
