DOC PREVIEW
UMD CMSC 433 - Specifications

This preview shows page 1-2-3 out of 9 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 9 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CMSC 433 – Programming LanguageTechnologies and ParadigmsSpring 2006Specifications2Specifications• “Without a specification your program cannot beincorrect. It can only do something unexpected.Look! A new feature!” -Gary McGraw3Software Specifications• A specification defines the behavior of an abstraction• This is the contract between user and provider– Provider’s code must implement the specification– Providers are free to change the implementation• So long as the new code still meets the specification– Users that depend implementation could be in trouble• Only rely on specification• Black box testing essentially checks compliance of animplementation with its specification4What Makes a Good Specification?• Sufficiently restrictive– Forbids unacceptable implementations• Sufficiently general– Allows all acceptable implementations• Clear– Easy to understand– A little redundancy may help (some people disagree)5Good Specifications are Hard and Rare• Very difficult to get people to write specifications– Even harder to keep them up to date• Having specifications in a separate document fromcode almost guarantees failure– Rationale for Javadoc: extract a standalonespecification from the code and embedded comments• Hard to accurately and formally capture allproperties of interest– Always finding important details not specified6Specifications Help You Write Code• Lots of subtle algorithms and data structures– Internal specs/invariants vital to correct implementation• Example: Binary Search Tree– All nodes reachable from left child have smaller keythan current node– All nodes reachable from right child have larger keythan current node7Specifications Help You Maintain Code• In the real world, much coding effort goes intomodifying previously written code– Often originally written by somebody else– Perhaps six different people have modified this code• Documenting and respecting key internalspecifications are the way to avoid a mess• Documenting and respecting key externalspecifications are the way to avoid having yourcustomers storm the office with torches andpitchforks8Formal vs. Informal Specificationsstatic int find(int[] d,int x)• An informal specification– If the array d is sorted, and some element of the array d is equal tox, then find() returns the index of x ……• A formal specification– (for all i, 0 < i < d.length, d[i-1] < d[i]and there exists j, 0 <= j < d.length, such that d[j] == x)implies find(d,x) = j ……9Advantages and Disadvantages• Formal specifications– Forces you to be very clear– Automated tools can check some specifications• Either at compile-time (static checking) or run-time(dynamic checking)• Informal specifications– Some important properties are hard to express formally• Sometimes just difficult• Sometimes don’t have the necessary formal notation– Some people are intimidated by formal specs10Types of External Specifications• Specifications on methods– Pre-conditions/requires: What must be true before call– Post-conditions/effects: What is must be true after call• Often relates final values to initial values// precondition: the array d is sorted// postcondition:// returnValue >= 0 && d[returnValue] == x// or (returnValue == -1 && x does not occur in d)static int find(int d[], int x);11Types of Internal Specifications• Specifications appearing within code itself– i.e., comments• Loop invariants: condition that must hold at thebeginning of each iteration of a loop– d[0..i] is sorted• Data structure or field invariants– elementCount <= elementData.length12Behavior vs. Function• Side effects– Writes output to a file– Could block on a condition or mutex• Performance– Should you specify performance of operations?– As hard as 451: what kind of bound (upper bound,amortized bound, expected bound, …), order of bound,…– But need at least informal specs• Random access is fast, insertion/deletion may beslow13Specifications and Subtyping• Liskov substitution principle (original? formal stmt)– If for each object o1 of type S there is an object o2 oftype T such that for all programs P defined in terms ofT, the behavior of P is unchanged when o1 issubstituted for o2 then S is a subtype of T.– I.e, if anyone expecting a T can be given an S, then S is asubtype of T.• If we ov erride a method, how do the specifications ofthe original and new method relate?14Specifications and Subtyping (cont’d) // precondition: the array d is sorted // postcondition: // returnValue >= 0 && d[returnValue] == x // or (returnValue == -1 && x does not occur in d)static int find(int d[], int x);• If we override this method, can the new method– Have true as a precondition?– Have precond “d is sorted and exists i s.t. d[i] == x”?– Have postcond “(returnValue==-1 and x does not occur in d)or returnValue is first index such that d[returnValue] == x”?– Throw NoSuchElementException rather than returning -1when x does not occur in d?15Javadoc• Integrates documentation into source code as comments• Will generate an external specification/** Javadoc Comment for this class */public class MyClass {/** Javadoc Comment for field text */String text;/** Javadoc Comment for method setText @param t Javadoc comment for parameter t*/public void setText(String t) {...}}16Javadoc example/** Given a sorted array, returns the indexinto the array of the given element,otherwise returns -1. @param d array to search in, assumed sorted @param x the element to search for @returns i >= 0 when d[i] == x, and -1 when x does not occur in d*/public static int find(int d[], int x) { …}17Javadoc example: HTML18A Few Javadoc Tags• Special tags for classes– @author– @version• Special tags for methods– @param– @return– @exception• Reference to another element–


View Full Document

UMD CMSC 433 - Specifications

Documents in this Course
Trace 1

Trace 1

62 pages

Reflection

Reflection

137 pages

Testing

Testing

25 pages

Paradigms

Paradigms

10 pages

Testing

Testing

17 pages

Java RMI

Java RMI

17 pages

Java RMI

Java RMI

17 pages

Java RMI

Java RMI

17 pages

Trace 1

Trace 1

46 pages

Jini

Jini

4 pages

Final

Final

15 pages

Java RMI

Java RMI

13 pages

Testing

Testing

16 pages

Load more
Download Specifications
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Specifications and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Specifications 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?