Quasi-boolean equivalence
Many program derivations are simplified if one allows the occurrence of certain Boolean subexpressions to which no value can reasonably be attributed. For instance, \(x\vee y\) ought to have the value true if \(x\) does, even if \(y\) is undefined. Such expressions are traditionally handled by the conditional connectives cand and cor, but these do not satisfy pleasant algebraic laws. The paper shows that it is safe to apply the rules for constructing equational proofs in the style of Dijkstra [\textit{E. W. Dijkstra} and \textit{C. S. Scholton}, Predicate calculus and program semantics, New York: Springer (1990; Zbl 0698.68011)] as if all subexpressions were well- defined. That is, possible undefinedness of subexpressions may be ignored.
- A logic covering undefinedness in program proofs
- scientific article; zbMATH DE number 3740740 (Why is no real title available?)
- scientific article; zbMATH DE number 46743 (Why is no real title available?)
- scientific article; zbMATH DE number 194642 (Why is no real title available?)
- Predicative methodology
- Programming as a Discipline of Mathematical Nature
- Quasi-boolean equivalence
- A note on undefined expression values in programming logics
- Properties of quasi-Boolean function on quasi-Boolean algebra
- Quasi-boolean equivalence
- scientific article; zbMATH DE number 718635 (Why is no real title available?)
- scientific article; zbMATH DE number 2102744 (Why is no real title available?)
This page was built for publication: Quasi-boolean equivalence
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2366071)
