Chapter 17
LePUS3 in Classical Logic
This chapter describes the relation between specifications in LePUS3 and the more general notion of specification in mathematical logic. We briefly introduce a notion of a first-order language, use it to unpack our notion of specification, and present the axioms of class-based programs.
17.1 LePUS3 AND CLASS-Z AS FIRST-ORDER LANGUAGES
Below we use a standard notion of a first-order predicate logic (FOPL) language. The set of logical symbols includes the logical connectives 
(conjunction), 
(disjunction), 
(implication), 
(biconditional), the quantifiers 
(universal), 
(existential), and the symbols for set {}, set membership ∈ and non membership 
equation =, and inequation ≠. The set of nonlogical symbols includes the binary superimposition operator ⊗ and ...
Get Codecharts: Roadmaps and blueprints for object-oriented programs now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
