17. models of the system


Write a similar schema for RESIZE. It should have the following informal semantics. The width and height attributes are of the shapes bounding box. The resize operation should make one corner of the bounding box be at the current mouse position (supplied as the argument current_pos?).

Hint: the width of a box is twice the difference between the x coordinate of the centre and the x coordinate of any corner:

 wid = 2 star | centre.x - corner.x | 


Strictly speaking, there are some errors in the Z usage for the hint in this exercise. The type Point is not a schema type, and so it is not meaningful to use schema selection, as in expressions like centre.x and corner.x. The alert Z student should pick up on this error. However, the spirit of the hint is still valid. To make things legal in Z, we can change the declaration of Point as follows:

|  x,y : R

To best specify this resizing operation, we will require to explicitly model the bounding box of a shape. We introduce a type, called BoundingBox which will represent the corners of the surrounding box which defines the extent of a shape. In fact, in Figure 17.1, we have drawn the bounding box for the circle but we have not made that information explicit in the specification in the text of this chapter. We omit details in this sample answer on 'rectangular' constraints for the corners of the bounding box (e.g., that upper left and right corners have the same y-coordinate values but the x-coordinate of the upper left corner is strictly less than the x-coordinate of the upper right corner, etc.)

|  upperleft, upperright,
|  lowerleft, lowerright : Point
|  upperleft.x less than or equal to upperright.x
|  upperleft.y = upperright.y
|  ...

We can add the bounding box as information known about shapes, by extending the definition of Shape. A constraint on the bounding box, motivated by the hint to this exercise, is that its width and height are the same as the width and height of the shape. In addition, the centre coordinates are related to the width and height. Note below that we use the names height and width in the definition of Shape to increase its readability.

|  type : Shape_type
|  width : R
|  height : R
|  centre : Point
|  bb : BoundingBox
|  width = 2 multiplied by (centre.x - bb.upperleft.x)
|  height = 2 multiplied by (centre.y - bb.upperleft.y)
|  width = (bb.upperleft.x - bb.upperright.x)
|  height = (bb.upperleft.y - bb.lowerleft.y)

Resizing can be viewed as changing the size of the bounding box. At a relatively abstract level, we can simply specify the resizing operation with a single argument indicating the new bounding box for the selected shape. A precondition for the operation is that there is only one selected shape.

|  State
|  State'
|  newbb? : BoundingBox
|  #selected = 1 
|  forallid : selected dot shapes'(id).bb = newbb?
|  forallid : (dom shapes - selected) dot shapes'(id) = shapes(id)
|  dom shapes' = dom shapes
|  selected' = selected

Other exercises in this chapter

ex.17.1 (ans), ex.17.2 (ans), ex.17.3 (ans), ex.17.4 (ans), ex.17.5 (tut), ex.17.6 (tut), ex.17.7 (tut), ex.17.8 (tut), ex.17.9 (tut)

all exercises for this chapter