Modular algebraic specification of some basic geometrical constructions

摘要

This paper applies some recent advances in algebraic specification technology to plane geometry. The two most important specification techniques are parameterized modules and order-sorted algebra; the latter provides a systematic treatment of subtypes. This exercise also indicates how a rigorous semantic foundation in equational logic can be given for many techniques in knowledge representation, including is-a hierarchies (with multiple inheritance), multiple representations, implicit (one-way) coercion of representation and parameterized modular structuring. Degenerate cases (which can be a particular nuisance in computational geometry), exception handling, information hiding, block structure, and pattern-driven rules are also treated, and again have rigorous semantic foundations. The geometric constructions which illustrate all this are specified over any ordered field having square roots of nonnegative elements; thus, we also specify some algebra, including rings, fields, and determinants. All specifications are written in a variant of the OBJ language.