Added simple vehicle example.
This commit is contained in:
parent
254d25ed97
commit
37544cf650
|
@ -12,6 +12,7 @@ projects.
|
|||
* **[ISP:](./isp)** A simple example of an ISP.
|
||||
* **[Royals and Loyals:](./royals_and_loyals)** The famous royals-and-loyals example.
|
||||
* **[Stack:](./stack)** A simple stack.
|
||||
* **[Vehicles:](./vehicles)** A simple modle of vehicles and driver's licenses.
|
||||
|
||||
## Team
|
||||
* [Achim D. Brucker](http://www.brucker.ch/)
|
||||
|
|
|
@ -0,0 +1,9 @@
|
|||
# Vehicles
|
||||
A simple modle of vehicles and driver's licenses.
|
||||
|
||||
## Data Sheet
|
||||
* Format: ArgoUML 0.26
|
||||
* Language: UML/OCL
|
||||
|
||||
For further information (license, citation, etc.), please look at the [README.md](../)
|
||||
of the main directory.
|
|
@ -0,0 +1,76 @@
|
|||
-- 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.
|
||||
|
||||
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
|
Binary file not shown.
Binary file not shown.
Reference in New Issue