A Teaching Tool for Specification Understanding
.
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.
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.)
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.
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;
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:
#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 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>;
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;
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;
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.
Page last updated March 11, 2010 by Chuck Cook