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 image (conjunction), image (disjunction), image (implication), image (biconditional), the quantifiers image (universal), image (existential), and the symbols for set {}, set membership ∈ and non membership image 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 O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.