Reminder:

• the implementor assumes it to be true...and codes accordingly
• the user must be sure in his code it is met in order to use

Postcondition: an assertion that prevails upon completion of the operation. A description of the results of the actions performed by the operation. It must be accurately and precisely stated

• the implementor must make it (through his code) true
• the user assumes it will be true

For the following specifications, we will assume that x is the instance to whom messages are being sent.

Conceptual module ComplexNumberKeeper begin imports type real exports type Complex method SetRealPartOfComplex method SetRealImaginaryPartOfComplex method RealPartOfComplex method ImaginaryPartOfComplex method CopyComplex method TestEqualComplex method AbsoluteValueOfComplex method AddComplex method SubtractComplex method MultiplyComplex method DivideComplex conceptual type Complex = (Re: real, Im: real) ... method RealPartOfComplex () : real pre true post RealPartofComplex = Re(x) method ImaginaryPartOfComplex () : real pre post ... method AbsoluteValueOfComplex () : real pre true post AbsoluteValueOfComplex = |x| method AddComplex (y: Complex) : var z: Complex pre true post z = x + y ... end

** var means that the stated variable will/can change

class Complex{ long re; long im; public ReComplex () { // pre: true // post: ReComplex = x.re return this.re ; } public ImComplex () { // pre: // post: ??? } ... public AddComplex (Complex y){ // pre: true // post: z.re = x.re + y.re // z.im = x.im + y.im ??? } }

Conceptual module ComplexNumberKeeper begin imports type real exports type NameOfComplex method NewComplex method DisposeComplex method SetRealPartOfComplex method SetRealImaginaryPartOfComplex method RealPartOfComplex method ImaginaryPartOfComplex method CopyValueOfComplex method SwapComplex method TestEqualComplex method AbsoluteValueOfComplex method AddComplex method SubtractComplex method MultiplyComplex method DivideComplex initially for all x:NameOfComplex,x is not a defined name conceptual type NameOfComplex = name of (real, real) method NewComplex () pre x is not a defined name post x is a defined name method DisposeComplex () pre x is a defined name post x is not a defined name method RealPartOfComplex () : real pre x is a defined name post RealPartofComplex = Re (Object (x)) ... method AddComplex (y: Complex) : var z: Complex pre x, y and z are defined names post Object (z) = Object(x) + Object(y) Object (x) = # Object(x) Object (y) = # Object(y) ... end

Conceptual module StackingQueueKeeper begin imports type Item exports type StackingQueue method Push method Enqueue method Dequeue method Concatenate method IsEmpty conceptual type StackingQueue = string of Item (conceptually looking at the structure as a String) intitially for all SQ: StackingQueue, |SQ| = 0 method Enqueue ( x: Item) // Note: this method would be called by SQ.Enqueue(x) in Java pre true post SQ = #SQ o x method Dequeue ( x: Item) pre |SQ| > 0 post #SQ = x o SQ method Push ( x: Item ) pre true post SQ = x o #SQ Note: this method would be called by SQ2.Concatenate(SQ1) in Java method Concatenate ( SQ1: StackingQueue) pre true post SQ2 = #SQ2 o SQ1 method IsEmpty () : booloean pre true post IsEmpty <=> |SQ| = 0 end

Conceptual module ListKeeper begin imports type Item exports type List method MoveToStart method MoveToEnd method Advance method Retreat method Get method Insert method Delete method SwapRemainder method AtStart method AtEnd conceptual type List = (string of Item, string of Item) intitially for all L: List, |L.Traversed| = 0 and |L.Remainder| = 0

Thus a List can conceptually be thought of as two parts: the items that have been traversed and the ones that have not (they "remain"). By specifying these two parts we provide a "marker" so we know where the list is at any time. (Like an index)

method MoveToStart () // Note: this method would be called by L.MoveToStart() in Java pre true post |L.Traversed| = 0 L.Remainder = #L.Traversed o #L.Remainder method MoveToEnd () pre true post |L.Remainder| = 0 L.Traversed = #L.Traversed o #L.Remainder method Advance () pre |L.Remainder| > 0 post |L.Traversed| = |#L.Traversed| + 1 L.Traversed o L.Remainder = #L.Traversed o #L.Remainder method Retreat () pre |L.Traversed| > 0 post |L.Remainder| = |#L.Remainder| + 1 L.Traversed o L.Remainder = #L.Traversed o #L.Remainder method Get( var x : Item) pre |L.Traversed| > 0 post there exists S: string of Item, such that L.Traversed = S o x

Note: This method does not Find an item x, it only Gets an item in the sense that it returns reference to the last item of the items Traversed. It does not really get anything in the sense that it does not take anything out of the List, the List stayed the same. How do I know this?

method Insert (x: Item) pre true post L.Traversed = #L.Traversed o x L.Remainder = #L.Remainder method Delete () notice no parameter, it simply deletes where it is pre |L.Traversed| > 0 post L.Remainder = #L.Remainder there exists x: Item, such that #L.Traversed = L.Traversed o x method SwapRemainders ( var L2: List) L1: instance got message pre true post L1.Traversed = #L1.Traversed L2.Traversed = #L2.Traversed L1.Remainder = #L2.Remainder L2.Remainder = #L1.Remainder method AtStart () : boolean pre true post AtStart <=> |L.Traversed| = 0 method AtEnd () : booloean pre true post AtEnd <=> |L.Remainder| = 0 end

Problem with "disjointness" We want to be able to use without knowing ADT implementation, but we need the type in order to declare properly (i.e., program that uses module and module must define type.)

(e.x. Say P1 uses modules M1 and M2. M1 declares type complex. Then one must have the type complex defined in P. These do not have to have the same name but must have the same definition. Unfortunately, if we change one definition, we must be sure to change the other)

Want loosely coupled (as little dependencies as possible)

Conceptual module for complex numbers

1. • Imagine that there are variables of type complex
   • variables used in calling programs can be declared as type complex
     (computationally the same)
2. • Don't imagine these variables hold objects there but x is re, im
   • instead variables hold names of objects x is and points to x.re and x.im

Advantage:
Won't have undefined objects because one really just has a skeleton if the type complex is present

• when creating an object, give a default value or say
  "no defined value"
• dynamic allocation

• Object is not created by saying x ... instead its just a place to put the name for one (need to allocate place for the object)
• To say r is unchanged
  r = #r     # designates old value
• Internal or private procedures
• note AddComplex in concept and in implementation