Graded Hoare Logic and its Categorical Semantics

AbstractDeductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.

Download Full-text

Synthesizing Conjunctive & Disjunctive Linear Invariants by K-means++ and SVM

The International Arab Journal of Information Technology ◽

10.34028/iajit/17/6/3 ◽

2020 ◽

Vol 17 (6) ◽

pp. 847-856

Author(s):

Shengbing Ren ◽

Xiang Zhang

Keyword(s):

Software Verification ◽

State Of The Art ◽

Positive Sample ◽

Machine Learning Algorithms ◽

Support Vector ◽

Hoare Logic ◽

Excellent Performance ◽

Automated Software ◽

Inductive Invariants ◽

Linear Invariants

The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically

Download Full-text

Proof Theory of the Cut Rule

10.1093/oso/9780198748991.003.0010 ◽

2018 ◽

Author(s):

J. R. B. Cockett ◽

R. A. G. Seely

Keyword(s):

Proof Theory ◽

Graphical Representation ◽

Basic Component ◽

Graphical Representations ◽

Mathematical Language ◽

Basic Logic ◽

Cut Rule ◽

Structural Rules ◽

The One ◽

Categorical Semantics

This chapter describes the categorical proof theory of the cut rule, a very basic component of any sequent-style presentation of a logic, assuming a minimum of structural rules and connectives, in fact, starting with none. It is shown how logical features can be added to this basic logic in a modular fashion, at each stage showing the appropriate corresponding categorical semantics of the proof theory, starting with multicategories, and moving to linearly distributive categories and *-autonomous categories. A key tool is the use of graphical representations of proofs (“proof circuits”) to represent formal derivations in these logics. This is a powerful symbolism, which on the one hand is a formal mathematical language, but crucially, at the same time, has an intuitive graphical representation.

Download Full-text

Polymorphic Iterable Sequential Effect Systems

ACM Transactions on Programming Languages and Systems ◽

10.1145/3450272 ◽

2021 ◽

Vol 43 (1) ◽

pp. 1-79

Author(s):

Colin S. Gordon

Keyword(s):

Algebraic Structure ◽

Position Effect ◽

Type Systems ◽

Sequential Effect ◽

Prior Work ◽

Sequential Effects ◽

Wide Range ◽

The Relationship ◽

Categorical Semantics

Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant. Understanding such systems in terms of a semilattice of effects grounds understanding of the essential issues and provides guidance when designing new effect systems. By contrast, sequential effect systems—where the order of effects is important—lack an established algebraic structure on effects. We present an abstract polymorphic effect system parameterized by an effect quantale—an algebraic structure with well-defined properties that can model the effects of a range of existing sequential effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems. We show that for most effect quantales, there is an induced notion of iterating a sequential effect; that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work; and that this induced notion of iteration is as precise as possible when defined. We also position effect quantales with respect to work on categorical semantics for sequential effect systems, clarifying the distinctions between these systems and our own in the course of giving a thorough survey of these frameworks. Our derived iteration construct should generalize to these semantic structures, addressing limitations of that work. Finally, we consider the relationship between sequential effects and Kleene Algebras, where the latter may be used as instances of the former.

Download Full-text