Red-Black-Tree model.

README.md

@@ -11,9 +11,11 @@ projects.
 * **[Digraph:](./digraph)** A simple tree like (recursive) data structure.
 * **[E-Bank:](./ebank)** A simple eBank/Accounting model.
 * **[Health System:](./health_system)** A simple health system.
+* **[Invoicing Orders:](./invoicing_orders)** A simple invoicing model.
 * **[ISP:](./isp)** A simple example of an ISP.
 * **[Mini Company:](./mini_company)** A tiny company example modelling a management hierarchy.
 * **[Priority Queue:](./priority_queue)** A simple priority queue model.
+* **[Red-Black-Tree:](./rbt)** A UML/OCL model of red-black-trees.
 * **[Royals and Loyals:](./royals_and_loyals)** The famous royals-and-loyals example.
 * **[Simple:](./simple)** A very simple toy example showing a few OCL syntax variations.
 * **[Simple Chair:](./simple_chair)** A simple conference management system.
@@ -21,7 +23,6 @@ projects.
 * **[Stack:](./stack)** A simple stack.
 * **[Vehicles:](./vehicles)** A simple model of vehicles and driver's licenses.
 
-
 ## Team
 * [Achim D. Brucker](http://www.brucker.ch/)
 

invoicing_orders/InvoicingOrders.ocl

@@ -0,0 +1,163 @@
+-- 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.
+-- 
+
+------------------------------------------
+-- 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
+

invoicing_orders/README.md

@@ -0,0 +1,46 @@
+# InvoicingOrders
+A simple invoicing model.
+
+## 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. 
+
+## The InvoicingOrders System
+This simple invoicing system is based on the book "Software
+Specification Methods: An Overview Using a Case Study" by M. Frappier
+and H. Habrias (ISBN 1-85233-353-7). 
+
+The InvoicingOrders system can informally described as follows: 
+1. The subject is to InvoicingOrders orders.
+2. To InvoicingOrders is to change the state of an order (to change it
+   from the state ``pending'' to ``invoiced'').
+3. On an order, we have one and one only reference to an ordered
+   product of a certain quantity. The quantity can be different to
+   other orders.
+4. The same reference can be ordered on several different
+   orders.
+5. 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.
+6. You have to consider the following two cases:
+   * **Case 1:** 
+     All the ordered references are references in the stock. The
+     stock or the set of orders may vary:
+     * due to the entry of new orders or canceled orders;
+     * due to having a new entry of quantities of products in
+       stock at the warehouse.
+
+     But, we do not have to take these entries into account. This
+     means that you will not receive two entry flows (orders, entries
+     in stock). The stock and the set of orders are always given to
+     you in an up-to-date state.
+   * **Case 2:**
+     You do have to take into account the entries of
+     * new orders;
+     * cancellations of orders;
+     * entries of quantities in the stock.
+
+  

rbt/README.md

@@ -0,0 +1,20 @@
+# Red-Black-Tree
+A model of red-black-trees in UML/OCL. This example is used in the paper 
+[Extending OCL with Null-References.](https://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.pdf) 
+for illustrating the use of 'null' in OCL 2.1.
+
+## Data Sheet
+* Format:               ArgoUML 0.26
+* Language:             UML/OCL (2.1)
+
+For further information (license, citation, etc.), please look at the [README.md](../)
+of the main directory. 
+
+## Publications
+* Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff. [Extending OCL with 
+  Null-References.](https://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.pdf) 
+  In Models in Software Engineering. Lecture Notes in Computer Science (6002), 
+  pages 261-275, Springer-Verlag, 2009. Selected best papers from all satellite 
+  events of the MoDELS 2009 conference.
+  https://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009
+  doi: [10.1007/978-3-642-12261-3_25](http://dx.doi.org/10.1007/978-3-642-12261-3_25)

rbt/rbt.ocl

@@ -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 rbt	    
+	
+  context RBTree 
+    inv wff:    not left.oclIsInvalid() and not right.oclIsInvalid()
+
+    inv redinv: color implies 
+                 ((left = null or not left.color)
+                   and (right = null or not right.color))
+
+    inv ordinv: (left = null or left.max() < key)
+
+    inv balinv: black_depth(left) = black_depth(right)
+
+  context RBTree::min(tree: RBTree):Integer
+    pre: tree<>null
+    post: isMember(tree, result) and
+          Integer::allInstances()->forAll(m:Integer | 
+	                           isMember(tree, m) implies result<=m)
+
+  context RBTree::max(tree: RBTree):Integer
+    pre: tree<>null
+    post: isMember(tree, result) and
+          Integer::allInstances()->forAll(m:Integer | 
+	                           isMember(tree, m) implies m<=result)
+
+ context RBTree::black_depth(tree: RBTree):Integer
+    pre: true
+    post: (tree = null and result = 0)
+          or (tree.left.color and result = black_depth(tree.left))
+          or (not tree.left.color and result = black_depth(tree.left) + 1)
+
+  context RBTree::isMember(tree: RBTree, a:Integer):Boolean
+    pre: true
+    post: result = tree <> null and (a = tree.key or isMember(tree.left, a) or isMember(tree.right, a))
+
+  context RBTree::insert(tree: RBTree, k : Integer):
+    pre:  tree <> null 
+    post: isMember(tree, k) and
+          Integer::allInstances()->forAll(m:Integer | m = k 
+	                        or (isMember(tree, m) = isMember@pre(tree, m)))
+
+  context RBTree::insertFail(tree: RBTree, k : Integer):
+    pre:  tree <> null 
+    post: isMember(tree, k) and
+          Integer::allInstances()->forAll(m:Integer | m = k 
+	                        or (isMember(tree, m) = isMember@pre(tree, m)))
+
+
+endpackage