ترغب بنشر مسار تعليمي؟ اضغط هنا

A New Perspective for Hoares Logic and Peanos Arithmetic

462   0   0.0 ( 0 )
 نشر من قبل Zhaowei Xu
 تاريخ النشر 2013
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English
 تأليف Zhaowei Xu




اسأل ChatGPT حول البحث

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.
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation logic with various forms of Presburger arithmetic constraints. Most significantly, we find that, even in the minimal case when we allow only conjunctions of simple difference constraints (xleq x+k) where k is an integer, polynomial-time decidability is already impossible: satisfiability becomes NP-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes P2-complete (P2 is the second class in the polynomial-time hierarchy) In fact we prove that the upper bound is the same, P2, even for the full pointer arithmetic but with a fixed pointer offset, where we allow any Boolean combinations of the elementary formulas (x=x+k0), (xleq x+k0), and (x<x+k0), and, in addition to the points-to formulas, we allow spatial formulas of the arrays the length of which is bounded by k0 and lists which length is bounded by k0, etc, where k0 is a fixed integer. However, if we allow a significantly more expressive form of pointer arithmetic - namely arbitrary Boolean combinations of elementary formulas over arbitrary pointer sums - then the complexity increase is relatively modest for satisfiability and quantifier-free entailment: they are still NP-complete and coNP-complete respectively, and the complexity appears to increase drastically for quantified entailments.
Weakly Aggregative Modal Logic (WAML) is a collection of disguised polyadic modal logics with n-ary modalities whose arguments are all the same. WAML has some interesting applications on epistemic logic and logic of games, so we study some basic mode l theoretical aspects of WAML in this paper. Specifically, we give a van Benthem-Rosen characterization theorem of WAML based on an intuitive notion of bisimulation and show that each basic WAML system K_n lacks Craig Interpolation.
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).
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا