overturetool / documentation Goto Github PK

The LRM says in Chapter 7

In the VDM interpreters the two subsets will always be chosen
such that they are non-empty and disjoint.

I'm afraid this explanation may give misunderstanding.
I first interpreted "they are non-empty" as "neither of the two subsets can be empty", but I think either subset can be empty, for example, {a} union rest should match against {1} with bindings a = 1 and rest = {}. A similar explanation is seen in munion.

A cursory look at the manual revealed the following problems:

• The Welcome page image (Fig. 2.1, pg.6) is outdated. The Welcome page no longer mentions sourceforge etc. (overturetool/overture#403).
• The outline image (Fig. 3.3, pg.9) is outdated. Function icons are now hollow (overturetool/overture#369).
• The POG chapter (chap.9) does not mention the auto-refresh mechanism (overturetool/overture#163). This feature is not in 2.1.6 but it should be in by the time of the next release.
• The GUI Builder feature (overturetool/overture#398) needs to be added. Should it have its own chapter or a section in Chapter 15?
• The command line control of the interpreter (overturetool/overture#351) also needs to be added. Maybe somewhere in chapter 16?
• PVJ: Update Code Generation chapter to reflect most recent changes to this plugin

Feel free to add anything else you find. We can create sub-issues and use this page to track progress towards the entire update.

concrete syntax definitions of class membership expressions (isofclass, isofbaseclass, sameclass, samebaseclass) lack commas between arguments. I made a pull request.
#5
Somebody please check and merge it. Thank you.

Currently we are working on updating the type checker to report an issue with the history expression - see overturetool/overture#472

As a consequence of this fix the CarNav* RT examples (there are two) do not type check anymore. For now I've simply excluded the tests from the ParseTcAllExamplesTest by indicating in the READMEs for these examples that the models do not type check - see da01ba2

That's fine for now. However, what we really need to do is to update the CarNav* examples such that they type check/execute again. The models ship with the tool so we should really fix the errors.

After the models have been fixed we should include them in the ParseTcAllExamplesTest again.

Hi,

When I was studying for my exam I noticed that the language manual does not define the behavior of writing mutex(opA) as a permission predicate, i.e., that opA is to be executed mutually exclusively to itself.

I suggest changing the line:
"A mutex predicate allows the user to specify either that all operations of the class are to be executed mutually exclusive, or that a list of operations are to be executed mutually exclusive to each other."

to:
"A mutex predicate allows the user to specify either that all operations of the class are to be executed mutually exclusive, an operation is to be executed mutually exclusive to itself, or that a list of operations is to be executed mutually exclusive to each other."

Furthermore, I suggest editing the example below the paragraph to include mutex(opA) (and changing the translated permission predicate accordingly).

Section 15.1.1 External Library Example gives example Java code but does not mention adding Overture jar to the class path, e.g.

javac -classpath "C:\Program Files\Overture\commandline\Overture-2.3.6.jar" sensor.java

The graphical version of the Conway example does not work.

This is because the jar is not a part of the example -- only the Java sources.

This is old news. See overturetool/overture#363

It somehow got closed. Anyway, we should fix it. We have canonical libs so all that's needed is to modify the VDMUnit file in this repo.

And then do the git submodule dace.

I don't find the "reverse" expression in the Operator Precedence section of LRM.
I suppose it should appear in the rhs of "sequence prefix operator" in C.3 and Table C.1.
I think precedence level of the "reverse" would be 6, which is the same precedence with the other sequence prefixes.
What precedence level is it implemented in Overture and VDMJ?

The graph-edSL example currently produces the following type errors.

Description	Resource	Path	Location	Type
Impure operation 'copy_compound_object' cannot be called from here.	graph-ed.vdmsl	/graph-edSL	line: 752	Problem
Impure operation 'copy_simple_object' cannot be called from here.	graph-ed.vdmsl	/graph-edSL	line: 755	Problem
Impure operation 'move_compound_object' cannot be called from here.	graph-ed.vdmsl	/graph-edSL	line: 676	Problem
Impure operation 'move_simple_object' cannot be called from here.	graph-ed.vdmsl	/graph-edSL	line: 679	Problem

The 2.5.0-release-candidate type-checker is right, and based on the name of the "move" operation it does not sound like it's right to make it pure either. Perhaps this model should use the classic dialect?

I just noticed that all the references are wrong in the available PDF version of the language manual.

Furthermore, the font appears to be different from the rest of the documentation.

I tried rebuilding the PDF through the Makefile and the PDF is attached here
VDM10_lang_man.pdf. It seems to be a minor oversight in the latest commit.

See Overture bug #667:

overturetool/overture#667 (comment)

As described in overturetool/overture#692 there's a problem with the grammar for sequence comprehensions. As pointed out by @nickbattle :

The sequence bind can bind multiple variables, but it can only do so via a simple bind, so that the > sequence is defined. So for example, you can say:

[ a+b | mk_(a, b) in seq [...] ]

But you cannot say:

[ a+b | a, b in seq [...] ]

But this constraint is not reflected by the LRM. This needs to be fixed.

The OvertureIDEUserGuide says that the POG view has a column with the proof status, which is ticked (discharged) if the PO matches one of a handful of trivial patterns. This was removed when the POG was updated to generate AST subtrees rather than strings - there is no such column in Overture 2.2.6.

A.1

There seems no point in defining any module, just have

document = module, {module}
         | definition block, {definition block}

A.4.1

type definitions is defined as

‘types’, [access type definition], {‘;’, access type definition}, [‘;’]

This would allow something like

types ; Pair = nat*nat

I think it is meant to be

‘types’, [access type definition, {‘;’, access type definition}, [‘;’]]

A similar comment applies to value definitions (A.4.3), function definitions (A.4.4), operation definitions (A.4.5) and traces definitions (A.4.9).
There is a slight inconsistency in syntax in that traces does not allow the optional trailing ‘;’ (which is probably better since the others use ‘;’ as both separator and terminator while traces only uses ‘;’ as a separator).

A.4.1/A.4.2

invariant and invariant initial function are defined twice identically, in A.4.1 and A.4.2.

A.4.4

Definition of identifier type pair list in A.4.4 could be simplified to

identifier type pair, {‘,’, identifier type pair}

A.4.4

There are two definitions of extended explicit function definition, one for VDM-SL and one for VDM++/VDM-RT. However, both definitions are identical.

A.4.5

I have never used operations so I am not sure but the definition of access operation definition seems rather strange

access operation definition = ( [ ‘pure’ ], [ ‘async’ ] [ access ], [ ‘static’ ])
                            | ( [ ‘pure’ ], [ ‘async’ ] [ ‘static’ ], [ access ]), operation definition;

A.4.9

Definition of trace definition term can be simplified to

trace definition, {'|', trace definition}

There is a spurious ';' character after the definition of trace binding definition

Missing ',' after 'let' in production trace let best binding

Definition of trace repeat pattern can be simplified to (last two lines)

| '{', numeric literal, [',', numeric literal], '}'

A.5.4

Unary expressions are defined as

unary expression = prefix expression
                 | map inverse;
prefix expression = unary operator, expression;
unary operator = ........
map inverse = ‘inverse’, expression;

A whole host of unary operators are defined, some are keywords, some are symbols. There seems no reason to factor out inverse into a separate production. Why is it not in the list of unary operators and the map inverse production dropped?

A.5.21

The term expression, [{‘,’, expression}] can be simplified to expression list

A.7.2

The term [{‘;’, assignment statement}] can be simplified to {‘;’,assignment statement}

In definition of multiple assign statement, a comma is missing before first assign statement

A.7.6

Spurious ',' at end of production call statement

A.8.1

map muinon pattern should be map munion pattern

B.2

Definition of is basic type can be simplified to ‘is_’, basic type

B.2

Definition of decimal literal can be simplified to numeral, ['.', numeral].....

The VCParser-masterSL example currently has a few parse errors. As this example bundles with the tool this issue should be fixed before the next release. I'd appreciate if someone who knows the model well can help out.

Thanks!

Hi all, my first time every posting on something like this so bare with me please!

In chapter 16 of the Overture VDM-10 Tool Support: User Guide there is are a couple examples of using a Remote Control class but the examples do not actually work for VDM_SL. in particular 16.3 uses the interpreter.execute("new A().op(123)") which is not allowed in SL (also class/module A isn't given so it's a little hard to work out how it should be used effectively). Later in 16.5 there is the interpreter.create("w", "new World()") and interpreter.valueExecute("w.Run()") which also both can't be used by VDM_SL.

My suggested improvements would be:

1. Clarify which VDM (type?) the given examples work for and which they don't

2. Add a more generic section a bit like Appendix I (really useful for my project!) for the functions you can call in the remote controller and what they do.

3. A VDM_SL specific example. E.g.

@OverRide
public void run(RemoteInterpreter interpreter) throws Exception {
this.interpreter = interpreter;
System.out.println("interpreter running");

           //sets the module MODULE_NAME as the default module to call methods from with the          interpreter
	this.interpreter.getInterpreter().setDefaultName("MODULE_NAME"); 

         //calls the method METHOD in the VDM module you are using with no input parameters
         interpreter.execute("METHOD()");

       //calls the method METHOD in the VDM module you are using with two input parameters
         interpreter.execute("METHOD( parameter1, parameter2)");

     //same as above but can concatenate strings
     interpreter.execute("METHOD( " + parameter[1] + " , " +  parameter[2] + ")");

    //get a value from the state or a type value
     interpreter.execute("state_variable.value"); -- e.g. current: <P1>|<P2>  in the state would be     
                                                                              interpreter.execute("current");

}

The easy way of thinking about it is typing into the console in overture but omitting the print before whatever you call. (I didn't try what happens with just typing state as that doesn't have print before it in overture :O)

I would post more specific examples but don't want to get told I plagiarised myself when I submit my dissertation because I uploaded some code on here or something! I was using these methods to make a simple GUI where I can press buttons to run the code rather than type everything in console particularly records which I have in a list I can just select from rather than type out 7 different record parameters each time, phew!

Also shout out to Leo Freitas who helped me solve the issue I'd had on all this.

The quick overview from https://github.com/overturetool/documentation/tree/editing/documentation/QuickOverviewVDMPPOperators

is inconsistent with the map operators, e.g. the language manual has the map operators '**' and 'comp', while the quick overview has not.