From e91414dc0d8227b9d2f985061fbb0efbb0b1292c Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 3 Oct 2016 01:09:25 +0100 Subject: [PATCH] Added ebank example. --- README.md | 1 + ebank/README.md | 11 ++++ ebank/ebank.ocl | 140 ++++++++++++++++++++++++++++++++++++++++++++++ ebank/ebank.pdf | Bin 0 -> 3714 bytes ebank/ebank.zargo | Bin 0 -> 5829 bytes 5 files changed, 152 insertions(+) create mode 100644 ebank/README.md create mode 100644 ebank/ebank.ocl create mode 100644 ebank/ebank.pdf create mode 100644 ebank/ebank.zargo diff --git a/README.md b/README.md index 4475df6..2401ff8 100644 --- a/README.md +++ b/README.md @@ -7,6 +7,7 @@ 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. diff --git a/ebank/README.md b/ebank/README.md new file mode 100644 index 0000000..d755cc2 --- /dev/null +++ b/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. + + diff --git a/ebank/ebank.ocl b/ebank/ebank.ocl new file mode 100644 index 0000000..02591ca --- /dev/null +++ b/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 diff --git a/ebank/ebank.pdf b/ebank/ebank.pdf new file mode 100644 index 0000000000000000000000000000000000000000..db1a32cc94b041129197f48244ea3fad3563f1ab GIT binary patch literal 3714 zcmb^!c~lc;-b!)Hw6#@~ids8ZF=$ODlVft21c87k1Y!U|Db*pFKp@G4$)p6tqLy~m zx&~{lB3>NoE@~^{0U{_;FYu@pL|Um@#VYEG?kZpf_nQ#$C~tTF@OzKPH^2M-eeqQ* zL)a)s0Qnxf?I?tVFc&5hQy`fP2`9`+bTW(qhz1EU7-@onkq{$J6G}o$>Ij7bveFcR zn;`qT9kF5LFCp(%|0}lLYx07Gf6i-;zdbB?Av`6~t*SFHYWI${j-0~W>zC5U)F+(X zHDlJ`x8jQOX5Gtg+E;rwBaL%^;FH5iEyTh3wyy5+ADVg|oPn2hG|wD zVpwy_ysXoXxiNEZ@U8~u{&KtR4dv16(s6u_W%v>@{F>%j=L&=`odP=)6&Z$H{LwXx?+X?pXC z`TT@vQ)83r#$J!wdb1rKfjkUvZ=fK=_-J0Q?T{VRs zCl|kyFu=pzEi>bwpTc|DzB0UEZ`q^H-{RTS)p47X zCf*l^rX}<>5+8?{wlbGH?{wc-~Ki>ZP(o+$q8@pPB}b^yb8y49p{Fr@Q8J{>Z>BApPfId z>C7I_8SDYYz6~;y@2tzGy{=a*t5UZ8!Gx^DzM=#}HwCYxC%VtL+*osMuyJ}^X zIX|>3T8P>1L-;2%`DI_kbxt1DJwsM9c4%n*ePOKU{m5J9?#Fd4F;70T@6Y{fp?a)s zO*{1+bau#{#P{p#hHk!BXm+cbaKN!U_Uu;?>h{fa$8x{h`h;u z%_)1;#j{(J24;+ISh={hXgFV4_`Xj;eV$HOq=}1+I$r)wo33=kl1uwWkMxke?zbr3 z*l65hn{y@XT7)=hr*^}H<;llBKm0Yvzg9lD=xcQ1CuuFGhu&G*RPa;#P(#*n&!8deY%Eyhj!()7T5pw_~Nhzn&3z-k6g`q_`{Al z<69FOzfu0>>rE?1$FtIwPH&lTFLQIAfxl#OTg(=!XU4Y9P`VBhp%dm2=?X&re5z^1ce4Qf9V|%;?{E8-Thr|N8PCn zi~iV?QyNBO)ZN@ots*W~Yt~*rJWg0X;{DHK_g^^GImxf0QqfKrWcz*?5l5un>qEPa+T%p)=rtq#cgu0<=gZgfXrt0Rl*hFw-!f8Q>72 zA*`g0(h^oM+SL@PjUwoH1Pp%|i6-ncAP=_FQ=@1w-eE~EM+gbHQAVZ)0>d5&0^dNO z6=s%%6Xddr(a^gzfG}Vd?6k`YBVh)e6^@4(t2Iyp3?$eXk&HAKE855E;taxR+(;%p z72z^oMbNkoU|^JCcwV>YMFG#efRISF3Pu$QmnOz3*Jjg*AcjrzoEeOlPqAW1{34e5 zbRh$AE5XDC2_=l560|{!JMBgo7=%RG5@{waOb~$PJ|~~^(zR7lo`|bZxDqb&w_9*+ zDnY}EM3TWQXWgwl$bte7rG{ye zG^QG8n8%TDP&Ue+1nVi>M5L2cDvWY477$74^imBdnqGn6OU_EBX^Rv=($mv9>3j}J zB_XIpB0;!3gvVn83br-FOyhR8+4>>S=QP9+*T-hIa-24Cw4@0!#33k$i#%1N1ny7< z3vD3HFryexByF^urPn4(L>M7pC+Y+eHi{A$n+pyb72;Ykit@!0Eb*x(%X1dKpb8*> zE{ zO3;mR7LUut*eH+9#ei1;7X%(%;1TvRP9f_4#VHoXs?a8;k@6e&fMNlp&J^&HnX4aE1 zlML`|n5Kl|WlG?)I3PHH8-NB0M1cZiPw~Gg5}2iLrE!XO2A&VX M2>JR3M}|QE0X_*myZ`_I literal 0 HcmV?d00001 diff --git a/ebank/ebank.zargo b/ebank/ebank.zargo new file mode 100644 index 0000000000000000000000000000000000000000..5740fa19eb33934d1a0557d10a3f0c526214443e GIT binary patch literal 5829 zcmZ{oWl$W2g%O4w_gxS#zCKgHP?{!P9{f3d4C^f-+k>)ttOq z=i*yGCmW}UnW?tFVfD7vMNf!P`{ugEv3X+;uE-^fF4j=EaLJ8osEe;r`D&;X2*+nh zJsYg(ASW3L6{C-`Rf=BPe^ot=He(_NC2iumRsn&jhl$Ejo+XF{l<;0#jE4Ora>chk z2x*%l{b2ooTjF&#U!agY&HawY8r))6(_;maeK+5Y#1pzAH|`zugEnEhwV*Xl?y)%6 zI!8lTjoLxt%^Ett{?hC~-t6jF!tcOl0*#vRXJe6q2Xux+i`6lK&}i?x4U*<29x%pc zd+g75N~I>1&OaOwWPCD&7vvX;)x$hgj$sGAb0&i_BlfJD675Nw_^|i*6hFnCwS1Dy z#?F=z{d zFPDr-V?M~Ll4RDhP?M(i4?JGy6wqh03#B~!IE~JStoKixrPGURV4+#G=P?!rM?%jRXfR4`$7rJld1pQHGs}(OOz5#MpPwkQy`*4}P z+)d$|zESiT2Yl)cW$HKu&>DFW-EXq~$a~EEp8OT7^Oja)=OXeV+=~Ax_U2a7m+Mw8 zd)MH+W#}`+=ht$s!0k;%871usd^Bim*rL}DNJlWG3^l&&l4kY3Q9sHm8`Gt2lWd^A z7yTGHc3*P1u|1N`eM7tpalg39cJ6EPGpBiVjlHQJtkQFCB6^OcP^J%BvI zmTmF5Fr`C7Gvs=)ce64yJ77d1)D+FgrAYJpp3N`x{a9n0ZgP|%yCCns*PAWGsweE4rnT~v~q7H0_ zZ!DQrrKpcRX4ohg?XFosA($3}lWgdYWw#4&R?#vk;^;ta)7nt}!5ZrSTLj^YU{hlk zOzQ)Evo_@EY2Oa58AKiW@gDoFU2I;y{N4jV;@J1NuK^GL=w;6=n08)Mc4 zWtW$}!cmZ4Zy`S_%JhX%n?>L-79$C@k#$c<<;_F^>#nf`EBhxF_I6HWT0y~{BtZ2< zPxVqFE4z)p>$lfnt!&TUPkLPH`5fwScyx@Kx>ME~YSNl+kB?pFjg#nBb2euc7IX#* zIG;vq`7V#!hqQ;=jSBr~0ejtJVMX<6|8NMm$7Fmd1{C5p1x=zLb=JRTW#-Z0ykQ-0 zERBzVP4HF=A@)?oHO>*b)wYSbitSoW%T?2JPb%kSTI7Lo?7o@tm14jC>>gGjonBb zec&U9HsBR0VJSqG{T^+=BeH=)(?LYk{=uRW6(b4N`K243Mo7Bm5-0?NrR9`)(4+{? zPkMdlnT1rPy{4(Xc2tOI6UB^%m#7yn)&+>f!vSMq;NQLnTZ~+aOkXswnGC?uDVo&+ zyX~PuCiEfCviXb_w_TXfj84gC}$|`XEGw3vzkOgYOOz{{H%iIkW@lq0=Zc0ybG5QkcLDIiR_Sz>##>czGxyW1z@SaURiHV z^t2BG9BO0!>32&AHGS_thZZ1260hB~?YiT4N%Ao=2s1ai#T{OVp8BXu={} zULtoM*%$OUWEYHwd-=$*1lwC9)_ko#WaNr5J zSUTf~@qVZfEuc_H%Us=Fj3A z^+I_KXeYi4X(J+{KMH{x|bN76QqqO5F5*E8NV~4VaNjq|VMCR2beLd#16scFV z6uml$YCKccPaxckxA6jnq_lOL@dEyv!)GnnVj|+a-m+&Aj&T1ifq~2)$q^#Or-ZWW zK1wQcISP*QtBHkSm@h`2%lDF0+W~hKcO98}JGEZOZ*innE=0j9)Rg27p+4NsQ4Hi$ zUq85~^d0aPK6jq_9=iZ*hO{gM>^d=3Hxk}CzR$gGSyHlHQD}YZP3--oi=wjWHQ9js z8GXU3{*C~CUnkq+sVVEKzfE=X`&c(Ocu81iNnNQ{FADR5HFz6&7Kk;LzYohKCWalV zPozGd%?Vx+(s43lZkgNKf(`$8=>+8nz1&Jj(DTfV_GXBzit%*{>#8?h4%e2p%JxtPsL1W`oy_) zQ6Z-H9Vbg8!10BQ@||87)A2bLf41-rm@ks1M2)OH@K6osyQSg|pN}75X-dKkEI4kDTmN zDUmy6Dn3}F8d|aA?ByKd1TQhW2TFN&oWIKSx#H#RdG$5|eqg(^HolEEK1u$$K-VNl zfc_ix=guWTQ4en>hn9|fMtDINKzs@)G<|@h`J6Ax{q#y^7QX~J6noYx3+-6b%v2|7 zsi2ln_`QCRf+bR)JFvCEMq&vgTwf`tVm?n%c}s3r@kTYH z3r2f0o!}R?=<+ZctvO`@O|7aFP~UV$a0aBCSMuSon*9Wj$mH^IAv)a8FZ^=x zlS95cOsFGUE-Mk&)$KFWOeWZ-HH@VPx`+Co8Tl0yhYiqr?8u21-qN0h&(N~Aa(VM{ zCbxRjom*tH{(8&^IO(np`$}x=;(a}Ho1tz(u)U&2m^O^ZBunmKipdQ6uG5=Dw+Y@- z+F92J)z;whx|yOKp+|=2j3*S`)zUyvJbWZJIOm8~W3@G{MW2lG4QsjF9?ifQXK*lv zV+)GMk}Szh!a9e= zCu_`Cofb?Dx1i@)kzVf6ZAf3`G1V@ZqRl|2$%vwR6O8w!AL~syjp<|_Rt^1aCftHH z9;1aV!w#1Ec{I%lKZ3(^?SyKIxW;x`PJ1+Gw7s~b zPq}Lxy)?R!bfIS}E$uaXkHy?cQGVZIy@ZXg;fJ!pso~44C#1g=J~I{2^%4gFfQ9{= z!U_M^XA0{-6wc%2XnSnz=$0i)__zXsL&P^dPBs7mSZBqpXZB?x$_w_B_TBClnzU+s z;8(@Ufe*^pYIDe;YIv0QtabXz?OaloGj`#;k3PB3Ns@k^`se$dx;h80Y9VP(G(*tZ zkQ&b-k}9?b_nU)_yGx~g@8|<0*Cxf0HzUV>on0STg>$Em_ltjEKIaRsMuF&;5!e&U zUT`7lL{9jJMqD&otJHH2@8*;)*_Ka69=6L^lmJJPI7bYR&r@0I)DH;=DG5O;llSdr zhbyFpsD$6piwvcM$KvC#N{%-^j*9vmw!Zm9^Lmg_zq;SzI)aGRKt)XYKj9`W;ZoH(` ztbzYGC~L}x&NG9we%GO7< zwoE7Wi|&gO5^S-Q=L>%QZ#s8|3L$(^xki33+`psF3&5|jL6rWwyAM!{1sM)#Mx;)% zQ)KOtva+bJdZo3XtmYVUqSKlCu4IIui3Ql z5LPlKVO7F&KNdzN^#7|i&e%~rpcF2|k0EfCPi7-sl7vlozo!3{;TC{&X-nk>t45VGW zGFSiYTh=}_3ra>rSF!XWkJZB7sm;zj}beOsn|{7aIp2x+n2 zpsajrjbUXaE*c-cA>+;I;NTQzfw25r>(op_EqaLhS4^OdfTy~=)g4qY*$#(HeSFKw zV;xmZn%7*kz$;NiZ6|)0Hdckwb7~8BH7kF3#+M{s=A;zdz8(D38{Tr#=k#@HpLW?E zn<5oqZo{Zew-TxLR%k5pH?;S72olIrGcK5;dOc8osS>e22G#y{u}eFD%MxY#>)m8t z`?gGq)fb}Ow{^>p*>oOZ1Y=cqa1X8Z|5BYcS3!kif!16ffcKprqpUz9q;O9QHx^oTYb!TF5`g7=1>J|#E{Jpn}?Hn?-r>P#ZPYOmD$)-8^K;V*vgtA3VFtg9E z(v`nxzmTh(wgKxYZ~x}3`jppv+RhPfOnv2cjA7$DKsRqqu(W?Q{bUx~8;amoJ#FGj zXCy#s<2DLm^Xxxap#Qlp@czu}KIE}2HWl=#NAR*=3K`w&kY=+q zFB)AhiLSjMK6cO^p1kbamJb+N)rSN_xG(7We^_o!T;U+CKSWU$0_)BWXO$!T1!IR3 z%Yj7eCVeDi)>1vEQSqY{>jrolz^V0*HL;<12}8=tj$T${%@0ct8&^$_nAfcPAzX3P z+B|Kt_V?G*-O;<>kGeV9qJYau;O9@q&u}Q{kLO`nvLQN?%UeXtc`Cbpe_ILJQdh^-g literal 0 HcmV?d00001