\documentclass{article} 
\usepackage{hyperref,graphicx,tabulary,alltt,endnotes,amsmath}
\setlength{\textwidth}{6in}
\setlength{\oddsidemargin}{0pt}

\setlength{\topmargin}{0pt}
\setlength{\headsep}{0pt} %if we ever use a head then get rid of this.
\setlength{\headheight}{0pt} %and this
\setlength{\textheight}{9in}

\hypersetup{ 
bookmarksnumbered, 
pdftitle={Procedure Specifications},
pdfauthor={Jose M Vidal},
pdfsubject={},
pdfkeywords={},
%FitBH=fit visible, FitH=fit width.
pdfview=FitH,
pdfstartview=FitH 
}
\newcommand{\hreffoot}[2]{\href{#1}{#2}\endnote{\href{#1}{}}}
\begin{document}
\title{Procedure Specifications}
\author{Jos\'{e} M. Vidal}
\date{Tue Jan 18 10:44:04 EST 2005}
\maketitle



      These slides are based on
      \begin{itemize}

	\item MIT 6.170: Open Courseware, \hreffoot{http://ocw.mit.edu/NR/rdonlyres/Electrical-Engineering-and-Computer-Science/6-170Laboratory-in-Software-EngineeringFall2001/E1DC2389-1837-4638-A27F-8900EE03EA5C/0/lecture04.pdf}{Procedure Specifications}
	\item MIT 6.170: Open Courseware, \hreffoot{http://ocw.mit.edu/NR/rdonlyres/Electrical-Engineering-and-Computer-Science/6-170Laboratory-in-Software-EngineeringFall2001/FFC1C94C-4CE0-4433-B40F-534AEC76D13F/0/lecture05.pdf}{Abstract Types}
      \end{itemize}
    \section{Introduction}



      \begin{itemize}
	\item Specifications are required for team work. 

	\item Many nasty bugs arise out of a misunderstanding about what
	something does. 

	\item Specifications are easier to read than code, so the client
	is happier. 

	\item Specifications allow the implementor to change her code
	without having to tell anyone. 

      \end{itemize}
    \section{Behavioral Equivalence}



      \begin{alltt}{\rm

static \textbf{int} \underline{findA} (\textbf{int} [] a, \textbf{int} val) \{
\textbf{  for} (\textbf{int} i = 0; i \(<\) a.length; i++) \{
  \textbf{  if} (a[i] == val)
    \textbf{  return} i;
  \}
\textbf{  return} a.length;
\}

static \textbf{int} \underline{findB} (\textbf{int} [] a, \textbf{int} val) \{
\textbf{  for} (\textbf{int} i = a.length -1 ; i \(>\)= 0; i--) \{
  \textbf{  if} (a[i] == val) \textbf{return} i;
  \}
\textbf{  return} -1;
\}   
}\end{alltt}
      \begin{itemize}
	\item Are these behaviorally equivalent?

	
	  \item \textbf{Not really} They
	    differ when \begin{ttfamily}val\end{ttfamily} is either missing or appears
	    more than once.

	  \item Still, it depends on the specification. They would be
	  equivalent if the specification was:
\begin{alltt}{\rm

requires: val occurs in a 
effects: returns result such that a[result] = val
}\end{alltt}
 

	
      \end{itemize}
    \section{Specification Structure}



      \begin{itemize}
	\item A precondition, indicated by the keyword \emph{requires}
	

	\item A postcondition, indicated by the keyword \emph{effects}
	

	\item A frame condition, indicated by the keyword
	\emph{modifies} 

	\item The precondition is an obligation of the client. 

	\item The postcondition is an obligation of the implementor of
	the method. 

	\item The frame condition identifies which objects may be modified. 
      \end{itemize}
    \section{Declarative Specifications}



      \begin{itemize}
	\item \textbf{Operational} specifications give a series of
	steps that the method performs. 

	\item \textbf{Declarative} specifications give properties of
	final outcome. 

	\item Prefer declarative. 

      \end{itemize}
      \begin{alltt}{\rm

public {\textbf{StringBuffer}} \underline{reverse}()
\emph{  // modifies: this
}
\emph{  // effects: Let n be the length of the old character sequence, the
  // one contained in the string buffer just prior to execution of the
  // reverse method. Then the character at index k in the new
  // character sequence is equal to the character at index n-k-1 in
  // the old character sequence.
}

\emph{  //Or, more formally
}
\emph{  //effects: length (this.seq) = length (this.seq )
  //for all k: 0..length(this.seq)-1 | this.seq [k] =
  //this.seq[length(this.seq)-k-1]
}}\end{alltt}

      \begin{alltt}{\rm

public \textbf{boolean} \underline{startsWith}({\textbf{String}} prefix)
\emph{  // Tests if this string starts with the specified prefix.
  // effects:
  // if (prefix = null) throws NullPointerException
  // else returns true iff exists a sequence s such that (prefix.seq ^
  // s = this.seq)
}
public {\textbf{String}} \underline{substring}(\textbf{int} i)
\emph{  // effects:
  // if i \(<\) 0 or i \(>\) length (this.seq) throws IndexOutOfBoundsException
  // else returns r such that
  // some sequence s | length(s) = i \&\& s ^ r.seq = this.seq
}}\end{alltt}
    \subsection{More Declarative Spec. Examples}



      \begin{alltt}{\rm

\emph{/*This one does not determine the outcome but it is
  still useful to clients. */}
public \textbf{boolean} \underline{maybePrime} ()
\emph{  // effects: if this BigInteger is composite, returns false
}

\emph{/*Same here, we don't know in which order they will be
    notified */}

public \textbf{void} \underline{addObserver}(\textbf{Observer} o)
\emph{  // modifies: this
  // effects: this.observers  = this.observers + \{o\}
}
public \textbf{void} \underline{notifyObservers}()
\emph{  // modifies the objects in this.observers
  // effects: calls o.notify on each observer o in this.observers
}}\end{alltt}
    \section{Exceptions and Preconditions}



      \begin{itemize}
	\item The most common use of preconditions is to demand a
	property because it would be hard or expensive to check
	it. 

	\item It is an engineering judgment. What is the cost of the
	check? what is the scope of the method? 

	\item 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)$. 

	\item Even when using a precondition, you might want to check it
	if it can de done speedily and easily. 
      \end{itemize}
    \section{Specification Ordering}



      \begin{itemize}
	\item Specification A is at least as strong as specification B if
      \end{itemize}
      \begin{enumerate}
	\item A's precondition is no stronger than B's

	\item A's postcondition is no weaker than B's, for the states that satisfy B's precondition. 
      \end{enumerate}
      \begin{itemize}
	\item That is, you can always weaken a precondition or strengthen a postcondition (make more promises).
      \end{itemize}
    \section{Judging Specifications}



      \begin{itemize}
	\item It should be \emph{coherent}. It should not have lots of
	different cases. 

	\item The results should be \emph{informative}. The effects
	should tell the client something about what it's doing. 

	\item The specification should be \emph{strong enough}. The
	modifies should be minimal: do as little as possible. 

	\item The specification should be \emph{weak enough} so that
	it can do what it promises to do most of the time (instead of
	failing).  
      \end{itemize}
    \section{User-Defined Types}



      \begin{itemize}
	\item All languages have built-in types. OO-languages allow one
	to define new types.

	\item The key idea of a \textbf{data abstraction} is that a
	type is characterized by the operations you can perform on
	it. 

	\item User-defined types are useful for achieving de-coupling. 
      \end{itemize}
    \section{Types of Types}



      \begin{itemize}
	\item A \textbf{mutable} type is one whose objects can be
	changed. An \textbf{immutable} type cannot be changed.

	\item In java \begin{ttfamily}Vector\end{ttfamily} is mutable but
	\begin{ttfamily}String\end{ttfamily} is immutable. 

	\item Immutable types are generally easier to reason
	about. 

	\item Mutable types might be faster to change, if large and
	change is only to a small part. 
      \end{itemize}
    \subsection{Types of Operations}



      \begin{itemize}
	\item \textbf{Constructors} create new objects of the
	type. 

	\item \textbf{Producers} create new objects from old
	objects. 

	\item \textbf{Mutators} change objects. 

	\item \textbf{Observers} take objects of the abstract type and
	return objects of a different type. 
      \end{itemize}
    \subsection{Example: List}



      \begin{alltt}{\rm

public \textbf{class} \textbf{List} \{
  public \textbf{List} ();
  public \textbf{void} \underline{add} (\textbf{int} i, {\textbf{Object}} e);
  public \textbf{void} \underline{set} (\textbf{int} i, {\textbf{Object}} e);
\emph{  // modifies this
  // effects
  // throws IndexOutOfBoundsException if i \(<\) 0 or i \(>\)= length (this.elems)
  // else this.elems  [i] = e and this.elems unchanged elsewhere
}
  public \textbf{void} \underline{remove} (\textbf{int} i);
  public \textbf{int} \underline{size} ();
  public {\textbf{Object}} \underline{get} (\textbf{int} i);
\emph{  // throws
  // IndexOutOfBoundsException if i \(<\) 0 or i \(>\) length (this.elems)
}
\emph{  // returns
  // this.elems [i] public void add (int i, Object e);
}  \}
}\end{alltt}
    \section{Designing and Abstract Type}



      \begin{itemize}
	\item Its better to have a few simple operations that can be
	combined in powerful ways. 

	\item Each operation should have a well-defined purpose. 

	\item The set of operations should be adequate to satisfy
	all. 

	\item The type may be either generic or domain-specific, but
	should not mix the two. 
      \end{itemize}
    \section{Representation Independence}



      \begin{itemize}
	\item \textbf{Representation Independence} means ensuring that
	the use of an abstract type is independent of its
	representation. 

	\item Changes in the representation should have no effect on the
	code outside the abstract type. 

      \end{itemize}
      \begin{alltt}{\rm

\textbf{Vector} v = \textbf{new} \textbf{Vector}();
\textbf{List} l = \textbf{new} \textbf{List} ();
....
v.copyInto (l.elementData);
}\end{alltt}
      \begin{itemize}
	\item This works as long as the List representation does not change.
      \end{itemize}
      \begin{alltt}{\rm

\textbf{class} \textbf{List} \{
  public \textbf{Entry} \underline{getEntry} (\textbf{int} i);
\}

\emph{//we can now write
}
\textbf{Entry} e = l.getEntry (i);
e.element = x;
...
e.element = y;
}\end{alltt}
      \begin{itemize}
	\item This is also bad because if the represenation changes
	there might no longer be Entry objects.

	\item The List class should only use Objects. 
      \end{itemize}
    \section{Language Mechanisms}



      \begin{itemize}
	\item Use \begin{ttfamily}private\end{ttfamily} to prevent access to data
	members. 

	\item Use \begin{ttfamily}interfaces\end{ttfamily} to achieve representation
	independence. 
	  \begin{itemize}
	    \item Interfaces don't have data members.
	    \item They also allow multiple implementations. 
	  \end{itemize}
	

	\item Since interfaces don't have constructors, it is wise to
	use the Factory pattern. 
      \end{itemize}
    \hrule
\theendnotes 
\hrule
\begin{small}
This talk is available at \url{http://jmvidal.cse.sc.edu/talks/specifications}\\
Copyright $\copyright$ 2004 Jose M Vidal.  All rights reserved.
\end{small}\end{document}
