Unknown error on VDM++ toolbox lite

106 views Asked by At

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 * nat1 ==>study
getsubj(numsubj,sem) == (
    subjpersem := numsubj/sem;
    );
end Course

I tried to run the code. Succeeded creating the object but when I run print getsubj(10,2), it returns error Run-Time Error 120: Unknown state component Can somebody help me thank you in advance

1

There are 1 answers

2
Nick Battle On

In Overture/VDMJ, this spec gives two type checking errors. Do these not appear in VDMTools?

Error 3247: Symbol 'subjpersem' is not an updatable variable in 'Course' (test.vpp) at line 9:5
Error 3027: Operation returns unexpected type in 'Course' (test.vpp) at line 7:8
Actual: ()
Expected: study
Type checked 1 class in 0.119 secs. Found 2 type errors