O'Reilly logo

Codecharts: Roadmaps and blueprints for object-oriented programs by J. Nicholson, Amnon H. Eden

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required