80 lines
3.1 KiB
Plaintext
80 lines
3.1 KiB
Plaintext
-- Copyright (c) 2003-2007 ETH Zurich, Switzerland
|
|
-- 2016 The University of Sheffield, UK
|
|
--
|
|
-- All rights reserved.
|
|
--
|
|
-- Redistribution and use in source and binary forms, with or without
|
|
-- modification, are permitted provided that the following conditions are met:
|
|
--
|
|
-- * Redistributions of source code must retain the above copyright notice, this
|
|
-- list of conditions and the following disclaimer.
|
|
--
|
|
-- * Redistributions in binary form must reproduce the above copyright notice,
|
|
-- this list of conditions and the following disclaimer in the documentation
|
|
-- and/or other materials provided with the distribution.
|
|
--
|
|
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
-- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
-- IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
|
-- DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
|
-- FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
|
-- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
|
-- SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
|
-- CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
|
-- OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
|
-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|
--
|
|
-- SPDX-License-Identifier: BSD-2-Clause
|
|
--
|
|
|
|
package Vehicles
|
|
|
|
context Person
|
|
inv AtLeastOneTruckPerPerson: self.truck->notEmpty()
|
|
inv NumberOfDrivenTrucksNotZero: self.truck->size() <> 0
|
|
inv AllPersonsWithDriversLicenseAdult:
|
|
self.driversLicense->notEmpty() implies self.age > 17
|
|
inv AllDriversAllowedToDriveTheirTrucks :
|
|
self.truck->forAll( t:Truck | self.isAllowedToDriveTruck(
|
|
self.driversLicense.licenseClass, t.oclAsType(Vehicles.Vehicle).tons))
|
|
|
|
context Person
|
|
inv FeatureOfLicenseClassCE:
|
|
Truck::allInstances()->forAll( t : Truck |
|
|
self.isAllowedToDriveTruck( 'CE', t.tons ) )
|
|
|
|
context Person
|
|
inv NoPersonMoreThan18Points:
|
|
self.ticket->iterate( t : Ticket ; sum : Integer = 0 |
|
|
sum + t.points ) <= 18
|
|
|
|
context
|
|
Person::isAllowedToDriveTruck(licenseClass:String, tons:Real):Boolean
|
|
post: result = if licenseClass='CE' or licenseClass='C'
|
|
then true
|
|
else if licenseClass='C1' or licenseClass='C1E'
|
|
then tons<=7.5
|
|
else false
|
|
endif
|
|
endif
|
|
|
|
context DriversLicense
|
|
inv AllLicenseOwnersAdult: person.age > 17
|
|
|
|
context Truck
|
|
inv MinimumDimension:
|
|
self.lengthLoadingSpace > 5.0 and self.widthLoadingSpace > 1.0 and
|
|
self.heightLoadingSpace > 2.0
|
|
inv MinimumCapacity: self.capacityLoadingSpace() > 10.0
|
|
|
|
context Truck::capacityLoadingSpace():Real
|
|
post: result = lengthLoadingSpace * widthLoadingSpace
|
|
* heightLoadingSpace
|
|
|
|
context Ticket
|
|
inv PointsNotNegative: self.points >= 0
|
|
inv NoTicketMoreThan18Points: self.points <= 18
|
|
inv NoTicketWithoutTruck: self.person.truck->notEmpty()
|
|
|
|
endpackage
|