diff --git a/README.md b/README.md index 494824b..fb041e9 100644 --- a/README.md +++ b/README.md @@ -15,6 +15,7 @@ projects. * **[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. diff --git a/rbt/README.md b/rbt/README.md new file mode 100644 index 0000000..41dfddb --- /dev/null +++ b/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) diff --git a/rbt/rbt-with-empty-tree-class.pdf b/rbt/rbt-with-empty-tree-class.pdf new file mode 100644 index 0000000..1791769 Binary files /dev/null and b/rbt/rbt-with-empty-tree-class.pdf differ diff --git a/rbt/rbt-with-empty-tree-class.zargo b/rbt/rbt-with-empty-tree-class.zargo new file mode 100644 index 0000000..45d0dce Binary files /dev/null and b/rbt/rbt-with-empty-tree-class.zargo differ diff --git a/rbt/rbt.ocl b/rbt/rbt.ocl new file mode 100644 index 0000000..1640bd0 --- /dev/null +++ b/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 diff --git a/rbt/rbt.pdf b/rbt/rbt.pdf new file mode 100644 index 0000000..d3c4f30 Binary files /dev/null and b/rbt/rbt.pdf differ diff --git a/rbt/rbt.zargo b/rbt/rbt.zargo new file mode 100644 index 0000000..4a6ae18 Binary files /dev/null and b/rbt/rbt.zargo differ