A logic covering undefinedness in program proofs
From MaRDI portal
Publication:790610
DOI10.1007/BF00264250zbMath0534.68024OpenAlexW2089387242MaRDI QIDQ790610
Publication date: 1984
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00264250
Other nonclassical logic (03B60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)
Related Items
Partial-predicate logic in computer science ⋮ Quasi-boolean equivalence ⋮ A simple sequent calculus for partial functions ⋮ A typed logic of partial functions reconstructed classically ⋮ Kleene's three-valued logic and process algebra ⋮ A note on undefined expression values in programming logics ⋮ Natural 3-valued logics—characterization and proof theory ⋮ Two over three: a two-valued logic for software specification and validation over a three-valued predicate calculus ⋮ Are the logical foundations of verifying compiler prototypes matching user expectations? ⋮ A guided tour of the mathematics of MetaSoft '88 ⋮ A logical framework for evolving software systems ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Empowering the Event-B method using external theories ⋮ Truth versus information in logic programming ⋮ Many-valued logic and mixed integer programming ⋮ On solvability of systems of partial fuzzy relational equations ⋮ Preservation of properties of residuated algebraic structure by structures for the partial fuzzy set theory ⋮ A completeness proof for a regular predicate logic with undefined truth value ⋮ An algebraic expression of finite horizon optimal control algorithm for stochastic logical dynamical systems ⋮ Inversive meadows and divisive meadows ⋮ A first order logic for partial functions ⋮ Proof obligations for blocks and procedures ⋮ Efficient Well-Definedness Checking ⋮ Modular structuring of VDM specifications in VVSL ⋮ Partial functions and logics: A warning ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ The connection between two ways of reasoning about partial functions ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ General correctness: A unification of partial and total correctness ⋮ Weak logic theory ⋮ Process algebra with four-valued logic ⋮ Partial logics reconsidered: A conservative approach ⋮ Proof systems for reasoning about computation errors ⋮ Missing values and dragonfly operations in fuzzy relational compositions ⋮ A first order logic for partial functions ⋮ Ours Is to Reason Why ⋮ Partial Functions and Equality in Answer Set Programming ⋮ Simple consequence relations ⋮ Reasoning about Separation Using Abstraction and Reification
Uses Software
Cites Work
- Partial abstract types
- An introduction to the PL/CV2 programming logic
- Edinburgh LCF. A mechanized logic of computation
- On a Formalization of the Non-Definedness Notion
- Separation properties and Boolean powers
- The Calculus of Partial Predicates and Its Extension to Set Theory I
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A logic covering undefinedness in program proofs
