What Does Any of This Have to do with Software Engineering?

There are many reasons that we are teaching you a bit about equational reasoning. First, it's a very simple and powerful proof technique, one with which you are familiar (in a different guise) from high school algebra and trigonometry. Because of its restricted set of formulae, axioms, and proof rules, equational reasoning can be semi-automated. Many theorem provers embody equational reasoning in terms of a semantics based on rewrite rules where equations are treated unidirectionally (e.g., the lefthand side rewrites to the righthand side). These theorem provers are used in the specification and verification of programs, hardware, and software systems.

Second, there is a class of models called algebras that are models for equational theories. An algebra is a pair, , of a set of values V and a set of functions, F. The equations in the theory determine when two values in the algebra are equal.

• Algebras are the foundational models of abstract data types (ADT's). From modern programming practice, we know it's good to structure programs around ADT's. One of the linchpins of all object-oriented methodologies is design using ADT's; thus, object-oriented design methods and programming languages owe their existence to algebraic models.
• Algebras are also the foundational model for some notions of concurrent processes. Later this term when we study CSP, we will look at one of these process algebras more carefully.

Finally, even though you may not build algebraic models of your systems, it's important to have in your arsenal a sense of algebraic properties of the entities in your system. Some standard algebraic properties of an operation on a system entity (like an object or a process) include: idempotency, reflexivity, symmetry, transitivity, commutativity, associativity, distributivity, existence of an identity element, and existence of an inverse relation or function. You are comfortable with algebraic properties of numbers, e.g., the commutativity and associativity of addition and multiplication for integers; it's just that there are similarly relevant algebraic properties that one can rely on, reason with, or prove about entities in computer hardware and software systems too.

For example, with respect to ADT's, you might want rely on the idempotency property of the insert(x) method on a set object; that is, if you insert x into the set multiple times you don't change the value of set object. Notice this property does not hold of a bag or stack or sequence or queue.

In the context of concurrent programs, it's reassuring to know that the parallel composition operator (||) is commutative, so that P || Q and Q || P denote the very same concurrent system. Notice of course that sequential composition (;) is not at all commutative (in most programming languages); thus, P; Q and Q; P will usually yield two different behaviors.

Thus, operations on entities like objects or processes that are modeled in terms of algebras enjoy algebraic properties.