Formal Methods -- SE304/CS407 -- Lab 3

Instructions

1. Form your own groups of size three. If you can't form a group of this size, contact a demonstrator and you will be assigned a group.

2. The lab has three questions, each with three parts. A question describes an Abstract Data Type (ADT) in English.

   • Part (a) asks you to informally specify (high level, mathematic specification) the ADT. It should take about twenty minutes.
   • Part (b) asks you to formally specify (JML specifications) the ADT. It should take about thirty minutes.
   • Part (c) asks you to refine the specification into a code implementation. It should take forty minutes.
   
   The time schedule is intended as a rough guideline and may be changed during the lab. When a part is completed, each person will be requested to stop working on that part and exchange their work with another member of the team.

3. Each person in the group should do just one part from one question. It is the responsibility of the person writing the implementation to hand up the completed assignment. It should be clearly documented who did what on each question.

4. For ease of coding, the ADT's can be constructed as collections of integer values. This allows you to hard code the types in the system. Your solution should scale to generic types (e.g. ADT of int, ADT of String, ADT of Object)

Questions

1. A Bounded Stack is an ADT that stores a collection of elements according to the last-in-first-out principle (i.e. only the last inserted element can be accessed or removed) that has an upper limit on the number of elements that can be inserted. Operations on the stack include:

   • max_size // largest number of elements
   • size // current number of elements
   • push // push element on stack
   • pop // pop element off of stack
   • top // get element at top of stack
   • reverse // turn stack upside down
   • split // divide the stack into some number of stacks
   
   (a)Provide a semi-formal, description of the structure.
   (b)Provide a formal JML specification of the structure.
   (c)Provide a refinement of the JML specification(implementation).
   



2. A Set is an ADT that stores a collection of elements (possibly infinite) without repetition of elements. Order in a set is irrelevant. Operations on the set include:

   • size // current number of elements
   • insert // put an element in the set
   • remove // take an element from the set
   • has // does the set have an element
   • compare // compare two sets for equality
   • union // union of two sets
   • intersect // intersection of two sets
   
   (a)Provide a semi-formal, description of the structure.
   (b)Provide a formal JML specification of the structure.
   (c)Provide a refinement of the JML specification(implementation).
   

3. A Sorted list is an ADT that keeps an order sorted list of items.

   • size // current number of elements
   • insert // put an element in the sorted list
   • remove // remove an element from the sorted list
   • has // sorted list has an element
   • count // number of times an element occurs
   • combine // combine two sorted lists
   
   (a)Provide a semi-formal, description of the structure.
   (b)Provide a formal JML specification of the structure.
   (c)Provide a refinement of the JML specification(implementation).
   

Home