The characterization problem for Hoare logics

Research by myself and by others has shown that there are natural programming language control structures that are impossible to describe adequately by means of Hoare axioms. Specifically, we have shown that there are control structures for which it is impossible to obtain axiom systems that are sound and relatively complete in the sense of Cook. These constructs include procedures with procedure parameters under standard ALGOL 60 scope rules and coroutines in a language with parameterless recursive procedures. A natural question to ask is whether it is possible to characterize those programming languages for which sound and complete proof systems can be obtained. For a wide class of programming languages and interpretations, it can be shown that P has a sound and relatively complete proof system for every expressive interpretation iff the halting problem for language P is decidable for all finite interpretations. Nevertheless, we are still far from a completely satisfactory characterization of the programming languages that can be axiomatized in this manner. The proof system that is generated in proving the above result does not have the property of being ‘syntax-directed’, which is distinctive of the Hoare axioms. Moreoever, theoretical considerations suggest that good axioms for total correctness may exist for a wider spectrum of languages than for partial correctness. In this paper we discuss these questions and others that still need to be addressed before the characterization problem can be considered solved.

Download Full-text

TOWARDS HIERARCHICAL DESCRIPTION OF SYSTEMS: A PROOF SYSTEM FOR STRONG PREFIXING

International Journal of Foundations of Computer Science ◽

10.1142/s0129054190000205 ◽

1990 ◽

Vol 01 (03) ◽

pp. 277-293 ◽

Cited By ~ 7

Author(s):

ROBERTO GORRIERI ◽

UGO MONTANARI

Keyword(s):

Proof System ◽

Simple Extension ◽

Levels Of Abstraction ◽

Complete Proof ◽

Proof Systems ◽

Action Refinement ◽

Atomic Action ◽

Description Languages ◽

Different Levels

The problem of relating system descriptions at different levels of abstraction is addressed in the context of process description languages. As a case study, we introduce two nondeterministic languages. The latter is a simple extension of the former and is obtained by adding to its signature an operator of strong prefixing for making atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, we introduce a mapping, called atomic action refinement, from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter, which can be homomorphically extended to become a mapping among process terms of the two languages. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process P and an atomic action refinement ρ, the refined process ρ(P) is proved to be an implementation of P. Moreover, two complete proof systems for the two languages (and thus also for the operator of strong prefixing) are presented and proved consistent with respect to refinement: if P and Q are congruent processes of the specification language, then ρ(P) and ρ(Q) are congruent, too.

Download Full-text

A survey of control structures in programming languages

ACM SIGPLAN Notices ◽

10.1145/987361.987363 ◽

1972 ◽

Vol 7 (11) ◽

pp. 1-13 ◽

Cited By ~ 9

Author(s):

David A. Fisher

Keyword(s):

Programming Languages ◽

Control Structures

Download Full-text

A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity

Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science ◽

10.1145/3373718.3394744 ◽

2020 ◽

Author(s):

Clemens Grabmayer ◽

Wan Fokkink

Keyword(s):

Proof System ◽

Regular Expressions ◽

Complete Proof

Download Full-text

A Complete Proof System for SCCS with Modal Assertions

Fundamenta Informaticae ◽

10.3233/fi-1986-9403 ◽

1986 ◽

Vol 9 (4) ◽

pp. 401-419

Author(s):

Glynn Winskel

Keyword(s):

Proof System ◽

Complete Proof

Download Full-text

On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽

10.3390/math9040385 ◽

2021 ◽

Vol 9 (4) ◽

pp. 385

Author(s):

Hyeonseung Im

Keyword(s):

Programming Languages ◽

Intuitionistic Logic ◽

Reference Point ◽

Classical Logic ◽

Proof System ◽

Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

Download Full-text

Complete proof systems for algebraic simply-typed terms

ACM SIGPLAN Lisp Pointers ◽

10.1145/182590.182482 ◽

1994 ◽

Vol VII (3) ◽

pp. 220-226

Author(s):

Stavros S. Cosmadakis

Keyword(s):

Complete Proof ◽

Proof Systems

Download Full-text

A characterization of the Poisson process

Journal of Applied Probability ◽

10.2307/3212584 ◽

1974 ◽

Vol 11 (1) ◽

pp. 72-85 ◽

Cited By ~ 13

Author(s):

S. M. Samuels

Keyword(s):

Poisson Process ◽

Renewal Process ◽

Poisson Processes ◽

Renewal Processes ◽

Sufficient Condition ◽

Necessary And Sufficient Condition ◽

Complete Proof ◽

Necessary And Sufficient

Theorem: A necessary and sufficient condition for the superposition of two ordinary renewal processes to again be a renewal process is that they be Poisson processes.A complete proof of this theorem is given; also it is shown how the theorem follows from the corresponding one for the superposition of two stationary renewal processes.

Download Full-text

A specification logic for concurrent object-oriented programming

Mathematical Structures in Computer Science ◽

10.1017/s0960129599002789 ◽

1999 ◽

Vol 9 (3) ◽

pp. 253-286 ◽

Cited By ~ 4

Author(s):

G. DELZANNO ◽

D. GALMICHE ◽

M. MARTELLI

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Linear Logic ◽

Operational Semantics ◽

Object Oriented ◽

Object Oriented Programming ◽

Higher Order Logic ◽

Specification Logic ◽

Theoretic Characterization

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

Download Full-text