Added ebank example.

README.md

@@ -5,7 +5,9 @@ models were developed in the context of the HOL-OCL and SecureUML
 projects.
 
 ## Models
+* **[Calendar:](./calendar)** A simple calendar/meeting model.
 * **[Company:](./company)** A simple company model, inspired by the OCL standard.
+* **[E-Bank:](./ebank)** A simple eBank/Accounting model.
 * **[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.

calendar/README.md

@@ -0,0 +1,9 @@
+# Calendar
+A simple calendar/meeting model.
+
+## Data Sheet
+* Format:               ArgoUML 0.26
+* Language:             SecureUML, ComponentUML
+
+For further information (license, citation, etc.), please look at the [README.md](../)
+of the main directory. 

calendar/calendar.ocl

@@ -0,0 +1,41 @@
+-- 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.
+
+-- source: calendar with secureUML
+
+package calendar
+
+-- class Entry (entity constraint)
+-- --------------------------------------------------------------------
+context Entry
+inv: (time.getCurrentHour() > 8) and (time.getCurrentHour() < 17)
+
+-- class EntryOwnerPerm (permission constraint)
+-- ---------------------------------------------------------------------
+context EntryOwnerPerm
+inv: self.ctxt.principal.identity.name = self.owner
+
+endpackage

ebank/README.md

@@ -0,0 +1,11 @@
+# The E-Bank
+A simple eBank/Accounting 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. 
+
+

ebank/ebank.ocl

@@ -0,0 +1,140 @@
+-- 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 eBank
+-- 
+-- Class Customer
+-----------------
+context Customer 
+  inv customer_must_have_account:   (self.accounts->size() > 0)
+  inv gender_impl_title: (gender implies (self.title = 'Mr.'))
+         and self.accounts->select(a:Account| a.oclIsTypeOf(eBank.CreditAccount))
+            ->collect(ca:Account| ca.getBalance())
+            ->sum() > -100000
+
+--
+-- Interface Account 
+--------------------
+context Account
+   inv:  owner.accounts->includes(self)
+
+context Account::makeDeposit(amount:Integer):Boolean 
+  pre:  amount > 0 
+  
+context Account::makeWithdrawal(amount:Integer):Boolean 
+  pre:  amount > 0
+
+--
+-- Class Transaction
+--------------------
+context Transaction
+  inv:  amount >= 0
+
+context Transaction::makeTransfer():Boolean 
+  pre:  source.getCurrency() = destination.getCurrency()
+        and 
+	source <> destination
+        and amount > 0
+ post:  ((source@pre.getBalance() - amount) = (source.getBalance()))
+        and 
+        ((destination@pre.getBalance() + amount) = destination.getBalance())
+  post: source.getBalance() + destination.getBalance()
+        = source@pre.getBalance() + destination@pre.getBalance()
+
+--
+-- Class BankAccount
+--------------------
+-- [Dresden] context BankAccount 
+-- [Dresden]  inv:  BankAccount.allInstances->forAll(a1,a2 | a1<>a2 implies 
+-- [Dresden]                                 a1.accountNumber <> a2.accountNumber)
+-- [Dresden]       -- alternative: Account.allInstances->isUnique(accountNumber)
+--
+-- [Dresden] context BankAccount::getBalance():Integer
+-- [Dresden]   post: result=balance
+
+-- [Dresden] context BankAccount::getCurrency():String
+-- [Dresden]  post: result=currency
+
+-- [Dresden] context BankAccount::makeDeposit(amount:Integer):Boolean
+-- [Dresden]    post: balance = balance@pre + amount
+
+-- [Dresden] context BankAccount::makeWithdrawal(amount:Integer):Boolean
+-- [Dresden]  post: balance = balance@pre - amount
+-- [Dresden]        and currency = currency@pre
+
+--
+-- Class CurrencyTradingAccount
+-------------------------------
+-- [Dresden] context CurrencyTradingAccount 
+-- [Dresden]  inv:  currency <> tradingCurrency
+
+-- [Dresden] context CurrencyTradingAccount::getTradingCurrency()
+-- [Dresden] post: result = tradingCurrency
+
+-- [Dresden] context CurrencyTradingAccount::buy(amount:Integer)
+-- [Dresden] pre:  amount > 0
+-- [Dresden] post: balance = balance@pre + price * amount
+
+-- [Dresden] context CurrencyTradingAccount::sell(amount:Integer)
+-- [Dresden]  pre:  amount > 0
+-- [Dresden] post: balance = balance@pre - price * amount
+
+--
+-- Class CreditAccount
+----------------------
+-- [Dresden] context CreditAccount 
+-- [Dresden]  inv:  creditLimit <= 0
+-- [Dresden]        and balance >= creditLimit
+-- [Dresden]       and self.book->size() < 21
+
+-- [Dresden] context CreditAccount::makeDeposit(amount:Integer):Boolean
+-- [Dresden]  pre:  amount <= maxAmount  
+-- [Dresden] post: if(creditLimit <= balance-amount) then
+-- [Dresden]           balance = balance@pre - amount
+-- [Dresden] 	    and
+-- [Dresden]            result  = true
+-- [Dresden]        else
+-- [Dresden]            balance = balance@pre
+-- [Dresden]          and
+-- [Dresden] 	    result  = false
+-- [Dresden]       endif
+
+--
+-- Class CheckBook
+------------------
+context Checkbook
+  inv:  self.checks->size() > 19
+        and self.checks->size() < 51
+
+--
+-- Class Check
+--------------
+context Check
+  inv:  self.checkbook->size() = 0
+        or self.checkbook->size() = 1
+
+endpackage