1 Replies - 1946 Views - Last Post: 06 May 2009 - 10:58 PM Rate Topic: -----

#1 blackout83  Icon User is offline

  • New D.I.C Head

Reputation: 0
  • View blog
  • Posts: 1
  • Joined: 06-May 09

VDM Implicit/Explicit operations help..

Post icon  Posted 06 May 2009 - 05:35 AM

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
return balance
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!!


Is This A Good Question/Topic? 0
  • +

Replies To: VDM Implicit/Explicit operations help..

#2 paperclipmuffin  Icon User is offline

  • Disassembling...
  • member icon

Reputation: 13
  • View blog
  • Posts: 944
  • Joined: 16-April 09

Re: VDM Implicit/Explicit operations help..

Posted 06 May 2009 - 10:58 PM

Please post your code between BBCode tags. It makes form easier reading. Like this:
your code here
Was This Post Helpful? 0
  • +
  • -

Page 1 of 1