I am new to programming, this site and VDM so help understanding this would be greatly appreciated!!
Ok so I kind of understand how explicit operations work within VDM - (fomal modelling software) but I am struggling to understand implicit operations and how they operate..
So an example of an explicit operation code in VDM here is..
Withdraw: nat ==> int --- Signature
Withdraw(amount) == --- parameter list
( balance := balance - amount; --- body
pre balance - amount > limit --- Pre-condition
So my question is when it comes to writing an Implicit operation, how do you go about constructing the operation??
Here is the same example, but of an Implicit operation.. (which I don't understand)
Withdraw(amount: nat) newBalance: int
ext rd limit : int --- ext stands for 'externals clause' rd stands for read..
wr balance : int --- wr stands for write, (what do they do?)
pre balance - amount > limit
post balance + amount = balance and newBalance = balance
Can anyone give me a detailled description of what is going on in this implicit operation. I dont get how to construct an implicit operation and need some advice!!
Page 1 of 1
1 Replies - 1718 Views - Last Post: 06 May 2009 - 10:58 PM
Replies To: VDM Implicit/Explicit operations help..
Page 1 of 1