166 lines
5.7 KiB
Plaintext
166 lines
5.7 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
|
|
--
|
|
|
|
------------------------------------------
|
|
-- Case 1
|
|
------------------------------------------
|
|
package InvoicingOrders
|
|
--
|
|
-- 1) Constraining the Data Model
|
|
-- ==============================
|
|
|
|
-- The stock of a Product is always a natural number, i.e., it is a
|
|
-- positive Integer. This also ensures the definedness of the stock.
|
|
context Product
|
|
inv isNat: self.stock >= 0
|
|
|
|
-- The Product id is unique.
|
|
context Product
|
|
inv idUnique: Product::allInstances()
|
|
->forAll(p1:Product, p2:Product | p1.id <> p2.id)
|
|
|
|
-- The quantity of an Order is always a natural number, i.e., it is
|
|
-- a positive Integer. This also ensures the definedness of the
|
|
-- quantity.
|
|
context Order
|
|
inv isNat: self.quantity >= 0
|
|
|
|
-- The state of an Order should either be `pending' or `invoiced'.
|
|
-- As a direct support for enumeration is not well developed in most
|
|
-- CASE tools, we use a String and constrain it to the two
|
|
-- alternatives using an invariant.
|
|
context Order
|
|
inv stateRange: (self.state = 'pending')
|
|
or (self.state = 'invoiced')
|
|
|
|
-- The Order id is unique.
|
|
context Order
|
|
inv idUnique: Order::allInstances()
|
|
->forAll(o1:Order, o2:Order | o1.id <> o2.id)
|
|
|
|
|
|
|
|
--
|
|
-- 2) Constraining the Dynamic Part
|
|
-- ================================
|
|
|
|
-- Initialize the state of an Order
|
|
context Order::state : String
|
|
init: 'pending'
|
|
|
|
-- Create a new Order
|
|
context Order::Order(prd:Product, qty:Integer):OclVoid
|
|
pre: qty > 0
|
|
pre: self.warehouse.products->exists(x:Product | x = prd)
|
|
pre: not prd.oclIsUndefined()
|
|
post: self.oclIsNew() and self.quantity = qty
|
|
-- and self.orderedProduct = prd
|
|
|
|
-- The state of the order will be changed into "invoiced" if the ordered quantity
|
|
-- is either less or equal to the quantity which is in stock according to the
|
|
-- reference of the ordered product.
|
|
context Order::invoice() : Boolean
|
|
pre: self.state = 'pending'
|
|
-- and self.quantity <= self.orderedProduct.stock
|
|
post: self.state = 'invoiced' and self.quantity = self.quantity@pre
|
|
-- and self.orderedProduct = self.orderedProduct@pre
|
|
-- and self.orderedProduct.stock = self.orderedProduct@pre.stock - self.quantity
|
|
|
|
-- Cancel order as an opposite operation to invoice order
|
|
context Order::cancel() : Boolean
|
|
pre: self.state = 'invoiced'
|
|
post: self.state = 'pending'
|
|
and self.quantity = self.quantity@pre and self.product = self.product@pre
|
|
and self.product.stock = self.product@pre.stock + self@pre.quantity
|
|
|
|
-- Create a new Order
|
|
context Product::Product():Boolean
|
|
pre : true
|
|
post: self.stock = 0 and self.oclIsNew()
|
|
|
|
-- Add quantity of the product to the stock
|
|
context Product::supply(qty:Integer):Boolean
|
|
pre: qty > 0
|
|
post: self.stock = self.stock@pre + qty
|
|
|
|
-- Remove quantity of the product from the stock
|
|
context Product::release(qty:Integer):Boolean
|
|
pre: self.stock >= qty
|
|
post: self.stock = self.stock@pre - qty
|
|
|
|
endpackage
|
|
|
|
|
|
-- ------------------------------------------
|
|
-- -- Case 2
|
|
-- ------------------------------------------
|
|
package InvoicingOrders
|
|
--
|
|
-- 1) Constraining the Data Model
|
|
-- ==============================
|
|
-- First, we present several invariants on the static data model. These
|
|
-- type constraints
|
|
|
|
-- There is one and only one Warehouse.
|
|
context Warehouse
|
|
inv isStatic: self.allInstances()->size() = 1
|
|
|
|
|
|
|
|
-- All products are in the Warehouse.
|
|
context Product
|
|
inv isInWarehouse :
|
|
not self.warehouse.oclIsUndefined()
|
|
|
|
-- -- All orders are in the Warehouse.
|
|
context Order
|
|
inv isInWarehouse: not self.warehouse.oclIsUndefined()
|
|
|
|
|
|
|
|
--
|
|
-- 2) Constraining the Dynamic Part
|
|
-- ================================
|
|
|
|
|
|
-- Create a new Order
|
|
context Order::Order(prd:Product,qty:Integer):OclVoid
|
|
pre: self.warehouse.products->exists(x:Product | x = prd)
|
|
|
|
|
|
-- Warehouse management
|
|
-- context Warehouse::getFirstInvoicable():Order
|
|
-- pre: self.orders->exists(x:Order |
|
|
-- x.state = 'pending' and x.quantity <= x.product.stock)
|
|
-- body: self.orders->any(x:Order |
|
|
-- x.state = 'pending' and x.quantity <= x.product.stock)
|
|
|
|
endpackage
|
|
|