Procedure Specifications

These slides are based on

• MIT 6.170: Open Courseware, Procedure Specifications
• MIT 6.170: Open Courseware, Abstract Types

Introduction

• Specifications are required for team work.
• Many nasty bugs arise out of a misunderstanding about what something does.
• Specifications are easier to read than code, so the client is happier.
• Specifications allow the implementor to change her code without having to tell anyone.

Behavioral Equivalence

• Are these behaviorally equivalent?
• Not really They differ when val is either missing or appears more than once.
• Still, it depends on the specification. They would be equivalent if the specification was:

  requires: val occurs in a 
  effects: returns result such that a[result] = val
  

Specification Structure

• A precondition, indicated by the keyword requires
• A postcondition, indicated by the keyword effects
• A frame condition, indicated by the keyword modifies
• The precondition is an obligation of the client.
• The postcondition is an obligation of the implementor of the method.
• The frame condition identifies which objects may be modified.

Declarative Specifications

• Operational specifications give a series of steps that the method performs.
• Declarative specifications give properties of final outcome.
• Prefer declarative.

More Declarative Spec. Examples

Exceptions and Preconditions

• The most common use of preconditions is to demand a property because it would be hard or expensive to check it.
• It is an engineering judgment. What is the cost of the check? what is the scope of the method?
• For example, binary search methods require that the array be sorted, otherwise they could not deliver $O(\log n)$. If they had to sort, it would be $O(n\cdot\log n)$.
• Even when using a precondition, you might want to check it if it can de done speedily and easily.

Specification Ordering

• Specification A is at least as strong as specification B if

1. A's precondition is no stronger than B's
2. A's postcondition is no weaker than B's, for the states that satisfy B's precondition.

• That is, you can always weaken a precondition or strengthen a postcondition (make more promises).

Judging Specifications

• It should be coherent. It should not have lots of different cases.
• The results should be informative. The effects should tell the client something about what it's doing.
• The specification should be strong enough. The modifies should be minimal: do as little as possible.
• The specification should be weak enough so that it can do what it promises to do most of the time (instead of failing).

User-Defined Types

• All languages have built-in types. OO-languages allow one to define new types.
• The key idea of a data abstraction is that a type is characterized by the operations you can perform on it.
• User-defined types are useful for achieving de-coupling.

Types of Types

• A mutable type is one whose objects can be changed. An immutable type cannot be changed.
• In java Vector is mutable but String is immutable.
• Immutable types are generally easier to reason about.
• Mutable types might be faster to change, if large and change is only to a small part.

Types of Operations

• Constructors create new objects of the type.
• Producers create new objects from old objects.
• Mutators change objects.
• Observers take objects of the abstract type and return objects of a different type.

Example: List

Designing and Abstract Type

• Its better to have a few simple operations that can be combined in powerful ways.
• Each operation should have a well-defined purpose.
• The set of operations should be adequate to satisfy all.
• The type may be either generic or domain-specific, but should not mix the two.

Representation Independence

• Representation Independence means ensuring that the use of an abstract type is independent of its representation.
• Changes in the representation should have no effect on the code outside the abstract type.

• This works as long as the List representation does not change.

• This is also bad because if the represenation changes there might no longer be Entry objects.
• The List class should only use Objects.

Language Mechanisms

• Use private to prevent access to data members.
• Use interfaces to achieve representation independence.
  • Interfaces don't have data members.
  • They also allow multiple implementations.
• Since interfaces don't have constructors, it is wise to use the Factory pattern.