Corrections/Improvements to Syntax Definition in LRM about documentation HOT 29 CLOSED

You're right about A.4.5 being peculiar, and there is a bug open about that elsewhere (presumably on the main Overture list, so it's good that it's captured here).

The original intent was to show that static and the access specifier could appear in either order. But when async and then pure were added, these were naively added to the grammar in a specific order. The parser actually allows all four tokens in any order (as long as there are no duplicates - which was the bug I referred to above). I think this parse is sensible. So the EBNF here should be changed to show "zero or more of these four things in any order".

from documentation.

The other bug is overturetool/language#40

from documentation.

For A4.1 ";" has always been used as a seperator (going all the way back to the ISO standard.

For A5.4 this has a historical reason. "map inverse" is the only unary operator which in the mathematical syntax is written AFTER the operand.

from documentation.

Some more comments.

A.1.1

Missing ',' in 'export functions signature', after 'functions'

A.1.1

Missing ',' in 'export operations signature', after 'operations'

A.2

confirm the definition, ‘,’ has higher precedence than ‘|’, should it perhaps be

(class | system), {class | system}

A.4.1

confirm the definition 'access type definition'; ‘,’ has higher precedence than ‘|’, should it perhaps be

([access],[’static’] | [‘static’], [access]), type definition

A.4.6

confirm the definition 'access assignment definition'; ‘,’ has higher precedence than ‘|’, should it perhaps be

([access],[’static’] | [‘static’], [access]), assignment definition

A.4.7

missing ‘,’ after ‘name list’ in 'mutex predicate'

A.4.8

second line of definition of 'periodic obligation' could be simplified to

‘(‘, 4 * expression, ‘)’

A.4.8

second line of definition of 'sporadic obligation' could be simplified to

‘(‘, 3 * expression, ‘)’

A.5

In the definition of ‘expression’, inset ‘narrow expression’ between ‘lambda expression’ and ‘new expression’

A.5.21

non-terminal (meta-identifier) 'pre-condition expression'; the character '-' is not allowed in meta-identifier names

A.7.2

missing ‘,’ after ‘(’ in 'multiple assign statement'

B.2

I think the definition of 'character literal' should be

character literal = "'", (character | escape sequence), "'"

B.2

In definition of 'escape sequence'

• missing ',' after '\x', '\u', '\c' and '\'
• confirm that empty term after the last '|' is intended
• Second line could be simplified to '2 * hexadecimal digit'
• Third line could be simplified to '4 * hexadecimal digit'
• Sixth line could be simplified to '3 * octal digit'

B.2

non-terminal (meta-identifier) 'Single-line comment'; the character '-' is not allowed in meta-identifier names

B.2

non-terminal (meta-identifier) 'Multi-line comment'; the character '-' is not allowed in meta-identifier names

from documentation.

An omission from the definition of type in A.4.1. There is an option for partial function type but not one for total function type. The grammar is such that for example nat +> nat is a valid type for a function but nat +> nat +> nat is not valid, nor is (nat +> nat).

from documentation.

Omission from the grammar. Section A.4.4.

The definition of extended explicit function definition does not include a measure clause.

Tested this in Overture and the measure clause is accepted.

from documentation.

Omission from the grammar. Section A.5.21.

The name of the function whose pre-condition is being used is omitted, immediately after 'pre_'. It should be

pre condition expression = ‘pre_’, name, ‘(’, expression, { ‘,’, expression }, ‘)’ ;

from documentation.

Attached is a consolidated list of the suggested changes (corrections and presentation improvements) to the VDM syntax in the LRM.

VDM-syntax.pdf

from documentation.

Thanks for doing all of this, Paul! I'm happy to help out with adding the corrections to the LRM. Anyone who wants to comment on the corrections before I do that?

from documentation.

from documentation.

A.5.21. Should 'name' be included but optional. If 'name' is not in the rule, where in the grammar am I allowed to create expressions like 'pre_f(1)'?

I think we still need 'is basic type', but maybe move it to A.5.19. Or else delete it and replace 'is basic type' in A.5.19 with 'is_', basic type.

from documentation.

"pre_f(1)" would parse as a normal function application, because the "pre_" reserved word does not (lexically) appear by itself. I agree that conflicts with the approach for "mk_R(1)", which has a footnote to say that there is no space after the "mk_". But if they didn't do that, record construction would parse as function application as well, which is very confusing. At least "pre_f(1)" is a function application!

Agree that A.5.19 should probably just say "is_", basic type, and we remove the other one.

from documentation.

Ok, I will revise items A.5.21 and B.2 (is basic type) to reflect this discussion.

Can you indicate how we should correct the definition of 'access operation definition' in A.4.5.

Note the last item (Overture Issue #632) requires a decision on which way to go. Any thoughts on that?

When all comments are received I will revise to give a final list to be reflected in the LRM.

from documentation.

Thanks, Paul. I appreciate that.

from documentation.

And if there was a small list of parser tweaks that we want made (as opposed to EBNF fixes, which don't affect the parser), that would help :)

from documentation.

All comments have been addressed. Attached is the final list.

VDM-syntax.pdf

from documentation.

Paul, thank you. I'll reflect it to the LRM repo in a couple of days.

from documentation.

Paul, as for A.4.1, my understanding is that total function type is not a type but can be placed at an explicit function's signature to declare that the function has total definition.

from documentation.

As for ‘access operation definition’, I don't see a good solution. So, I skip it for now.

from documentation.

I suspect the new periodic/sporadic obligation is not equivalent to the original. I skip it.
I suspect 'RESULT' is an implicitly declared identifier. If it is, we'll need to write up a section for that in the "expression" chapter. I'm skipping it for now.
"pre-condition expression" is corrected to "precondition expression" which is used in other places.

from documentation.

I updated the LRM on the repository.
Please check https://github.com/overturetool/documentation/blob/editing/documentation/VDM10LangMan/VDM10_lang_man.pdf

from documentation.

Thanks Tomo. Looks good. Some minor corrections.
VDM-syntax.pdf

from documentation.

Concerning your comments.

1. Total Functions
   It would surprise me if +> is not a type. That would mean we are able to specify a function as total, but not specify the the argument or result type of a higher order function is total, which severely constrains the utility of having +>. Note that Overture does not impose this constraint, and I have used it extensively in my specifications. Take a filter function on sequences, of type (ignoring totality)

seq of @a * (@a->bool) -> seq of @a

I see no reason why we should not be able to stipulate that the predicate is total (it becomes a proof obligation). If not, the function itself can never be total. What we would like is

seq of @a * (@a+>bool) +> seq of @a

A question for PGL I think.

2. periodic/sporadic obligation (A.4.8)
   I got that wrong. What I meant to say was

periodic obligation = 'periodic', '(', 4 * expression, ')', '(', name, ')';

and similar for sporadic obligation.

3. RESULT
   I made that proposal because RESULT is listed explicitly as a keyword in the grammar (B.2), and it is presented as bold dark red in Overture like other keywords. As you say, needs clarification.

from documentation.

One more thing, in the definition of escape sequence in B.2, there is an empty clause after the last '|'. I can't see any reason why that should be there, but I may be missing something. Can we confirm it is correct or change.

from documentation.

Related to this are Overture issue #632 and Language issue #40. I think we should endeavour to address these for the 2.5 release as well.
overturetool/overture#632
overturetool/language#40

from documentation.

done :-)

from documentation.

done with periodic/sporadic obligation :-)

from documentation.

Concerning the total function type I ca say that in the ISO standard this is only available in the context of defining a function and even here totality means in relation to a potential pre-condition. The difference between partial and total functions was only introduced in the ISO VDM-SL standard in order to enable the description of a functional style interpreter of a language containing loop constructs (where you naturally would not be able to guarantee totalness in relation to the halting problem). We can naturally decide to have both total and partial functions present inside type definitions but then they would be slightly different from that used in a function definition (where a pre-condition can be present).

from documentation.

LRM changes were included with release 2.5.0.

from documentation.