A Semantic Analysis of Logics That Cope with Partial Terms

Abstract

Specifications of programs frequently involve operators and functions that are not defined over all of their (syntactic) domains. Proofs about specifications –and those to discharge proof obligations that arise in justifying steps of design– must be based on formal rules. Since classical logic deals only with defined values, some extra thought is required. There are several ways of handling terms that can fail to denote a value — this paper provides a semantically based comparison of three of the best known approaches. In addition, some pointers are given to further alternatives.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{JonesLS12,
  author       = {Cliff B. Jones and
                  Matthew J. Lovert and
                  L. Jason Steggles},
  editor       = {John Derrick and
                  John S. Fitzgerald and
                  Stefania Gnesi and
                  Sarfraz Khurshid and
                  Michael Leuschel and
                  Steve Reeves and
                  Elvinia Riccobene},
  title        = {A Semantic Analysis of Logics That Cope with Partial Terms},
  booktitle    = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
                  Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7316},
  pages        = {252--265},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-30885-7\_18},
  doi          = {10.1007/978-3-642-30885-7\_18},
  timestamp    = {Mon, 03 Mar 2025 20:58:01 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/JonesLS12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}