Note: This is based on the instructor's solution for Problem 4 on Exam 1in CSci 658 (Software Language Engineering) in Fall 2013 Exam 1. (This was a take-home exam.)
The module defines the semantics of the CandyBowl abstract data type (ADT) using (a) invariant assertions to characterize valid states of its instances (between ADT function calls), (b) precondition and postcondition assertions to characterize function behavior. The invariants are implicitly conjuncted to the preconditions and postconditions of the functions.
An ADT invariant must be true for any bowl ADT instance in the argument list at the time of the call or any bowl instance returned at the time of the return.
An ADT interface invariant specifies the required value (i.e., state) of the ADT instance in terms of an abstract model of the ADT and more primitive functions in the public interface. The interface invarient should be the same for any implementation of the ADT.
For Carrie's Candy Bowl I use the howMany function
to formalize the invariant.
An ADT Interface Invariant for CandyBowl bowl can be stated as
(ForAll c: validCandyType(c) :: howMany(bowl,c) >= 0)
and (Sum c,n: n == howMany(bowl,c) :: n) == howMany(bowl)
where validCandyType(c) has an appropriate definition.
An ADT Implementation Invariant complements the interface invariant by defining the abstract features in terms of concrete variables and data structures. The implementation invariant is implicitly conjuncted with the interface invariant.
I also define the semantics of the ADT functions using precondition
and postcondition assertions. A precondition must hold at the time of
the call and may reference the arguments. A postcondition must hold
at the time of the return and may reference both arguments and the
return values. I prefix an argument instance with arg_ and a
returned instance with return_.
The ADT function howMany is sufficient for specifying a
constructive semantics for all functions except itself. To formalize
the ADT fully, a better approach would be to use the mathematical
concept of bag (or multiset) to model a candy bowl instance's state.
(See the notes on the bag concept.)
A minimal way to hook a bag model into our invariants might be to AND
the following conjunct into the Interface Invariant:
(ForAll c : validCandyType(c) ::
howMany(bowl,c) == OCCURRENCES(c,CandyBowlBag))
This new conjunct specifies the relationship between the Lua data
structure bowl and the mathematical bag CandyBowlBag used to model
the candy bowl instance.
In this assertion, function OCCURRENCES(c,B) denotes the number of
copies of element c occurring in bag B.
Perhaps the various preconditions and postconditions should be restated in terms of CandyBowlBag properties instead of "howMany", but that did not seem to be necessary.
(1) Function CandyBowl(bowl) returns a new empty
candy bowl if the argument bowl is nil or unspecified;
otherwise, it returns a shallow copy of the argument
bowl. The argument bowl is not
modified. The functionality of returning a copy of an existing bowl is
not required by the specification.
Pre: arg_bowl == nil or arg_bowl satisfies ADT invariants
Post: if arg_bowl == nil then howMany(return_bowl) == 0
else (ForAll c: validCandyType(c) ::
howMany(return_bowl,c) == howMany(arg_bowl,c))
Reminder: The interface and implementation invariants are implicitly ANDed into both the precondition and the postcondition of each function for each instance of CandyBowl.
(2) Function has(bowl,candyType) returns true if and
only if bowl contains one or more pieces of type
candyType candy. The argument bowl is not
modified.
Pre: validCandyType(candyType) Post: return == (howMany(arg_bowl,candyType) > 0
(3) Function put(bowl,candyType,n) adds integer
n pieces of candyType candy to the argument
bowl. n defaults to 1 if nil or
unspecified.
Function put modifies its argument bowl, but
function putcp returns a modified shallow copy of the argument
instead. Note: The description does not specify whether the function
can mutate its table argument; these two functions implement both
possibilities.
Pre: validCandyType(candyType) and (n == nil or n > 0)
Post: ( if n == nil then
howMany(return_bowl,candyType) == howMany(arg_bowl,candyType) + 1
else
howMany(return_bowl,candyType) == howMany(arg_bowl,candyType) + n )
and
(ForAll c: validCandyType(c) and c ~= candyType ::
return_bowl[c] == arg_bowl[c])
and
return_bowl == arg_bowl
By return_bowl == arg_bowl, I mean they are the same
table, not that their attributes are identical.
(4) Function take(bowl,candyType) removes one piece
of candyType candy from the argument bowl.
Function take modifies its argument
bowl. Function takecp returns a modified
copy of the argument bowl instead. Note: The
specification does not specify whether the function can mutate its
table argument; these two functions implement both possibilities.
Pre: validCandyType(candyType) and howMany(arg_bowl,candyType) > 0
Post: (howMany(return_bowl,candyType) == howMany(arg_bowl,candyType) - 1 ) and
(ForAll c: validCandyType(c) and c ~= candyType ::
return_bowl[c] == arg_bowl[c]) and
return_bowl == arg_bowl
By return_bowl == arg_bowl, I mean they are the same table, not
that their attributes are identical.
(5) Function howMany(bowl,candyType) returns the number of pieces
of candy that are in the bowl overall if
candyType is nil; otherwise, the function returns the
count of the pieces of candyType candy that are in the
bowl.
Pre: candyType == nil or validCandyType(candyType)
Post: if candyType == nil then
return == (Sum c,n: validCandyType(c) and n == howMany(arg_bowl,c) :: n)
else return == number of candyType candies in arg_bowl
Note: To formalize "number of candyType candies in
arg_bowl" in the postcondition, we need a richer abstract model
for the ADT. We currently use the
howMany(bowl,candyType) function to specify the other
functions. As discussed in the Better Approach section, one approach
is to use the mathematical concept bag (or multiset) to model the ADT.
With that model, we can restate the postcondition as:
if candyType == nil then
return == (Sum c,n: validCandyType(c) and n == howMany(arg_bowl,c) :: n)
else return == OCCURRENCES(candyType,CandyBowlBag)
(6) Function isEmpty(bowl) returns true if and only
if the bowl is empty.
Pre: true Post: howMany(bowl) == 0(7) Function
inventory(bowl) returns a list-style table
of pairs {candyType, count}candyType.
Pre: true
Post: validInventory(return) and
(ForAll c,n: howMany(arg_bowl,c) == n and n > 0 ::
(Exists i: i > 0 :: return[i] == {c,n}) )) and
(ForAll i,c,n: 1 <= i <= #return and return[i] == {c,n} ::
howMany(arg_bowl,c) == n) )
where
validInventory(inv) == inv ~= nil and type(inv) = "table" and
(ForAll i: i < 1 or i > #inv :: inv[i] == nil) and
(ForAll i: 1 <= i <= #inv ::
(Exists c,n: inv[i] == {c,n}:: validCandyType(c) and n > 0) )
and
(ForAll i: 2 <= i <= #inv :: inv[i-1][1] < inv[i][1]) )
(8) Function combine(bowl1,bowl2) returns the bowl
resulting from pouring bowl1 and bowl2
together to form a new bowl.
Pre: true (i.e., both bowl1 and bowl2 satisfy interface invariant)
Post: (ForAll c ::
howMany(return_bowl3,c) == howMany(arg_bowl1,c) + howMany(arg_bowl2,c) )