Questions tagged [vdm++]
A language for the design and specification of systems, based on the Vienna Development Method. VDM++ supports object-oriented and concurrent specifications. The VDM language is supported by the Overture Tool.
40
questions
0
votes
2
answers
57
views
VDM++ type error: The state component "totalPrice" must not be used here
I wrote a code which is for the total price of book when multiplied by number of book and the book price in VDM++.
class Book
types
public Title = seq of char;
instance variables
private ...
0
votes
1
answer
34
views
How to model accepting a pdf file as input in VDM++
Let say I want to model a program that will accept a file of type pdf.
How should I model accepting a pdf file as input in VDM++?
0
votes
1
answer
39
views
How to use precondition to ensure that the inputs are of type int only
Let say I have a function that return the lesser of two input values of type int. I want to set the precondition to only allow a and b of type int.
class Example
functions
min: int * int -> ...
0
votes
1
answer
93
views
Is there type casting in VDM++?
For example, I want to cast nat to seq of char in VDM++.
In the code below, I want operation setValueOfX to return "X is {value of q}", if q is of type nat and q < 3.
class A1
instance ...
1
vote
2
answers
170
views
Set/sequence summation operator?
I have a set, S = { 1, 2, 3, 4, 5 }.
If I wanted to sum this in standard logic it's just ∑S (no MathJax on SO so I can't format this nicely).
What's the VDM equivalent? I don't see anything in the ...
0
votes
1
answer
111
views
How do I transform/operate on a set/sequence?
I have a set S = { 1, 2, 3, 4, 5 }.
What is the syntax for changing the contents of the set (or rather, creating a new set) by applying a mathematical operation to it e.g. multiplication, power?
1
vote
1
answer
51
views
How can I apply a predicate to a set?
Say I have a set, S = { 1, 2, 3, 4 } (the contents don't really matter)
I can say forall x in set S & x mod 2 = 0 but that will give me a boolean answer - are all the numbers in it even? What if ...
1
vote
1
answer
40
views
Pure operation call may not be referentially transparent?
I get this warning when i try to use a pure operation on the two first elements of a sequence.
The code looks something like this:
class A
functions
public func: Seq -> bool
func(sq) == (
(...
0
votes
1
answer
73
views
Can't return each element from a set when running it through a for all loop
I am trying to return each element from a set containing Brewage objects by running it through a for all loop. But the return value gets messed up when i try to do so.
The loop function:
public ...
0
votes
1
answer
48
views
i have two errors in vdm sl project , 1) Action = <OPEN_BARRIER>; 2) Time :: hour : nat;
smart parking model in vdm-sl
types
Id = token;
Status = <EMPTY> | <OCCUPIED>;
Type = <A> | <B> | <C> | <D> | <E>;
Node :: id : Id
status : Status
...
0
votes
2
answers
183
views
Printing to console in VDM++?
How do I print text or values to the console to validate that my model is working correctly?
I would like to do something like this:
class Main
operations
public Run: () ==> ()
Run() ==
...
0
votes
2
answers
338
views
How to install Overture on Windows
I'm running Widows 7 Professional on a 64-bit system with Java SE 10. I downloaded Overture-2.6.2-win32.win32x86-64.zip and unzipped it under c: and clicked on the Overture application. It started and ...
1
vote
1
answer
69
views
Unknown error on VDM++ toolbox lite
I'm doing VDM++ on VDM++ toolbox lite and below is my example code:
class Course
types
public study :: numsubj : nat1
sem : nat1;
public subjpersem = nat1;
operations
public getsubj:nat1 *...
0
votes
1
answer
74
views
Pre-condition not working
I'm trying to create a simple 'signup' method.
-- Creates a new account
public signup: String * String ==> ()
signup(username, password) == (
-- create user
dcl user: User := new User(...
0
votes
1
answer
122
views
Use cases in operations in VDM++
Im pretty new to VDM++ and im trying to use cases in a operation to see how it works.
My idea was to give the operation an input and see what it gave me as output. So fx. my input could be: and I ...
2
votes
1
answer
325
views
A recursive function in VDM
How would I define a recursive function to find the biggest power of two less than an input number in VDM?
The function is as follows:
largest: N -> N
All I've got so far is:
largest(n) =
if n=...
0
votes
2
answers
567
views
Set comprehension in VDM++
I've defined 2 types:
public string = seq1 of char;
public config = map string to bool;
I've also defined a test set: dcl subFeatures : set of string := {"test1", "test2", "test3"}.
And I'm trying ...
0
votes
1
answer
301
views
Instance variable is not initialized. Why is that?
I got this problem with my instance variables. They will not be initialized and I'm unsure what is exactly means. It's the same for every class I have. I posted one of the codes below:
class Good
...
0
votes
1
answer
98
views
Specifikation of operation in VDM++
I would like to know what the operations mean in the picture. Most what the line, 'getStartPrice()== (return startPrice)' mean.
I'm really new too this.
0
votes
2
answers
111
views
Modelio and Overture, does it work separately?
So.. I’m trying to work with both Modelio and Overture but both programs is really new to me.
I want to make a model in Modelio as a first, and then export it to Overture.
But is it supposed to work ...
0
votes
1
answer
74
views
How to round a real number?
Say I wanted to round a real number to a natural number, how could I do this in VDM++? The MATH library does not appear to have any function that does this.
Thanks,
Ricardo
0
votes
1
answer
164
views
Overture error: Name 'BinBuilder()' is not in scope
I've been doing the exercises of a book focused on iteratively building a whole application. After having written four classes, I'm writing my fifth which is a test for the fourth one. However, ...
1
vote
2
answers
121
views
Execution in the presence of type bindings
Consider the two function definitions
test1 (x:nat) res:set of nat
== { m | m:nat & m in set {0,...,x} };
test2 (x:nat) res:set of nat
== { m | m in set {0,...,x} & true };
...
1
vote
4
answers
561
views
Recursive call stack depth
I have a recursive function that works for input where the call stack depth is up to 1000, but fails for bigger inputs. I converted the function to be tail recursive and that allowed it to get to ...
1
vote
1
answer
95
views
Difference between = and <=> in extended implicit function definition
I see some interesting behaviour with an extended explicit function.
I define an implicit function
isLeap (year:nat) res:bool
post res = year rem 4 = 0 and (year rem 100 = 0 => year rem 400 ...
1
vote
0
answers
238
views
modelio does not import overture uml exported file
I want to learn how to use Modelio and Overture together to learn to model programs with UML and VDM. The whole procedure about creating a UML model, exporting it to XMI (uml extension), and importing ...
1
vote
1
answer
73
views
Import module from different project in Overture
When I import one module from another in Overture all is quite straightforward. However, I can't work out how to import a module from another project. What I do is:
create project P1
create module A ...
1
vote
1
answer
110
views
Overture and Mathematical Syntax
Is it possible to use the VDM mathematical syntax with Overture or is it restricted to the ASCII syntax.
Alternatively, when generating LaTeX, can the mathematical syntax be used for the output?
I ...
0
votes
1
answer
72
views
Overture tool on Debian crashes everytime
I have installed Debian 7 on my computer. I installed Overture tool by downloading and extracting the .zip file. Every time I try to run Overture I get the following error message:
# A fatal ...
-1
votes
1
answer
85
views
Overture/Stackoverflow/VDM projects corrupted/vanished
I've spent the past 2 weeks working on a coursework for College, I had pretty completed 90% of it. I decided to open Overture now and seems like all my projects have corrupted :((((((
http://gyazo....
1
vote
1
answer
243
views
What does opposite angle brackets <> mean?
Example 1
forall x,y in set {1,…,5} & X <> y => not m.temps(x) = m.temps(y)
Example 2
exists i,j in set inds m.temps & i <> j and m.temps(i) > 400 and m.temps(j) > 400
...
1
vote
2
answers
444
views
VDMSL Recursive function minimum value of sequence
I think this should be relatively straightforward, was wondering if anyone knew how to answer this:
Define a recursive function seq-min : N+ -> N which returns the smallest value in a sequence of ...
0
votes
2
answers
120
views
Formal methods - Map of price relating cars to price with two sets BL and Fiat
I have a question from Chapter 5 in Practical Formal Methods with VDM by Derek Andrews and Darrel INCE which I was unsure how to answer, so here it is, thanks for any help!
If the map price relates ...
0
votes
1
answer
442
views
VDM++ Toolbox: Operation or function is not in scope using example Tree implementation
I'm using the Tree definition, that comes with The VDM++ Toolbox v9.0.2 and, when trying to use the function addRoot() (using the interpreter), on the first usage, I always get the error: "Run-Time ...
1
vote
1
answer
198
views
VDM++ language semicolon
I am reading a manual of VDM++ language. My question is this in some cases he use ";" at the end of statement and somewhere in the same statement he is not using ";".
Below is the example
public Top ...
0
votes
1
answer
105
views
Temperature logical expressions
I'm working on some logical expressions. I want to merge 2 expressions into one but not right sure how.
I am using the VDM Overture Tool.
I am looking at set of 5 temperatures. Some are over 400, ...
-2
votes
1
answer
567
views
how to write function in VDM++ language [closed]
I am making a translator of VDM++. which converts VDM++ code in C++. For that i am doing mapping of VDM++ into C++.
I want to know how to write a function in VDM++?
for example.
float functionX(int ...
0
votes
1
answer
273
views
VDM++ clock time
I implemented a random number generator in vdm++. But I wanted to the seed to be the clock time from the computer. Does anyone know if there is a equivalent vdm++ function to c++ function time(NULL)?
...
1
vote
1
answer
255
views
Error in Constructor VDM++
I'm getting a stupid error in VDM++ ToolBox Academic.
When I try to run an operation it gives me this error:
Run-Time Error 280: No constructor with this parameter list is in scope
value: "Game"
My ...
1
vote
1
answer
454
views
Generate random number in vdm++
Does anyone know how to generate a random number in vdm++? The math library doesn't work for me.