Homework 4

How many people can visit the canteen?

• 200

• 1

• No limit

Must every student visiting the canteen eat a dish?

• Yes

• No

How many dishes can the canteen offer?

• 3

• 1

• No Limit

How many drinks can a person take?

• 3

• 1

• No Limit

Invariant 1:

context Dish

inv : student_price < 5

• Satisfies

• Does not satisfy

Invariant 2:

context Canteen inv : self . dishes -> select ( type = Type :: vegetarian )

-> collect ( students ) -> size () = 2

• Satisfies

• Does not satisfy

Invariant 3:

context Canteen inv : self . guests ->

exists ( guest : Person | guest . diet = Type :: vegan )

• Satisfies

• Does not satisfy

Invariant 4:

context Canteen inv : self . dishes ->

forAll ( d : Dish | d . students -> notEmpty () implies d . students . host ->

notEmpty ())

• Satisfies

• Does not satisfy

Invariant 5:

context Employee inv : self . in_homeoffice = true implies self . host -> isEmpty ()

• Satisfies

• Does not satisfy

Invariant 6:

context Canteen inv : self . revenue_students = self . dishes ->

iterate ( d : Dish ; inc : Integer = 0| if( d . students -> size () > 0) then inc + d . student_price * d . students -> size () else inc endif )

• Satisfies

• Does not satisfy