One of the software engineering objectives of all
undergraduate curricula in computing is to at least expose students to formal
specifications of behavior. These specifications are presented formally in
mathematical logic and can be written in a variety of formal specification
languages. A simple tool to teach specification understanding with a
variety of exercises is available at
this link.

#### The Basic Idea with Examples

Given below are two example specifications of operations in
the RESOLVE notation. All specifications rely on mathematical
conceptualization (or modeling) of programming objects. In the first
example, programming integers are mathematically conceptualized as taking
values from Z (the set of mathematical integers), except that they’re
constrained to be within Min_Int and Max_Int. In the **ensures**
clause, #I denotes the incoming value of I whereas I denotes its current
value (i.e., the value after in the ensures clause).

**Operation** Increment(**updates** I: Integer);
**requires** I < Max_Int;

**ensures** I = #I + 1;

If Max_Int were to be a 1000, for example, then to show an understanding of the specification, one could give a listing of valid inputs and expected outputs, such as the following:

These input-output pairs also serve as specification-based test cases for the operation.

The second one is a data abstraction example. Here, a Queue of entries is conceptualized as a mathematical string of entries. Mathematical string notations we commonly use include empty_string to denote a string containing no entries, alpha o beta (or alpha * beta) to denote the concatenation of two strings, |alpha| to denote the length of a string alpha, and <x> to denote a string containing a single entry x. (The specification mode**alters** allows an implementation the
flexibility to alter the entry E to have an arbitrary value after the
operation, whereas the **restores** mode would demand that it remain
the same.)

**Operation** Enqueue(**alters** E: Entry; **updates** Q: Queue);
**requires** |Q| <= Max_Length;

**ensures** Q = #Q o <#E>;

If Max_Length equals 5 and entries are Integers, then on valid input #E = 7 and #Q = <3, 4>, Q will become <4, 7, 3>. E could be any Integer.

Dequeue specification states that the Entry E is replaced with a new value. It also illustrates that specifications are assertions and that “=” is not assignment as in programming.

**Operation** Dequeue(**replaces** E: Entry; **updates** Q: Queue);
**requires** |Q| > 0;

**ensures** #Q = <E> o Q;

Once introduced to examples such as the ones above, formal specification understanding can be demonstrated for more interesting exercises, especially with operations whose names are no communicative.

**Operation** Mystery_2(**updates** E: Entry; **updates** Q: Queue);
**requires** |Q| > 0;

**ensures** there exists Rst Str(Entry) such that
#Q = <E> o Rst and Q = <#E> o Rst;

A more compelling use of these ideas is to help students understand a mathematical abstraction of lists, in which lists are conceptualized as a pair of strings of entries.

#### Experimentation and Tools

A tool to teach specification understanding with a variety of exercises
(including ones for a list abstraction) is available
at this link. This
specification understanding tool is also named Test Case Reasoning
Assistant (TCRA). It lets a user provide valid inputs and expected
outputs for a given specification, and checks if they satisfy the
specification. When a combination fails, it shows why and when it
succeeds it shows how it worked. The tool can be used with RESOLVE
specifications as above or with Java style specifications, where
every operation is implicitly parameterized by a “self” object. We
have used the tool in our software engineering classrooms at Clemson,
but classes on data structures, algorithms, and programming with
objects can use the tool as well.

We appreciate your feedback on this tool as well as suggestions for several more exercises. Please contact Dana Leonard (GRA and tool developer), Jason Hallstrom, or Murali Sitaraman

This research is funded in part by a National Science Foundation CCLI grant.

If Max_Int were to be a 1000, for example, then to show an understanding of the specification, one could give a listing of valid inputs and expected outputs, such as the following:

#I

-3

0

3

999

-3

0

3

999

I

-2

1

4

1000

-2

1

4

1000

These input-output pairs also serve as specification-based test cases for the operation.

The second one is a data abstraction example. Here, a Queue of entries is conceptualized as a mathematical string of entries. Mathematical string notations we commonly use include empty_string to denote a string containing no entries, alpha o beta (or alpha * beta) to denote the concatenation of two strings, |alpha| to denote the length of a string alpha, and <x> to denote a string containing a single entry x. (The specification mode

If Max_Length equals 5 and entries are Integers, then on valid input #E = 7 and #Q = <3, 4>, Q will become <4, 7, 3>. E could be any Integer.

Dequeue specification states that the Entry E is replaced with a new value. It also illustrates that specifications are assertions and that “=” is not assignment as in programming.

Once introduced to examples such as the ones above, formal specification understanding can be demonstrated for more interesting exercises, especially with operations whose names are no communicative.

A more compelling use of these ideas is to help students understand a mathematical abstraction of lists, in which lists are conceptualized as a pair of strings of entries.

We appreciate your feedback on this tool as well as suggestions for several more exercises. Please contact Dana Leonard (GRA and tool developer), Jason Hallstrom, or Murali Sitaraman

This research is funded in part by a National Science Foundation CCLI grant.

Page last updated March 11, 2010 by