Request for Modification: set1 type

[paulch42]

Identification of the Originator

Paul Chisholm

Target of the request, defining the affected components of the language definition

Affects type 'set' and its primitive functions.

Motivation for the request

It is common in specifications to define functions that require a non-empty set as argument. This requires a pre-condition of the form "s <> {}". If a type 'set1' (non-empty sets) was introduced such constraints could then be captured in the type alone.

Description of the request

Add the type 'set1' to the VDM-SL language.

description of the modification

The definition of the 'set' type is enhanced to include 'set1'. Modification would be as for the type 'seq1' with respect to sequences.

benefits from the modification

Simplifies the specification of functions that require non-empty sets as argument. Would avoid some testing for empty set where result type guarantees non-empty. More consistent with the approach taken for 'seq/seq1'. The primitive function 'dinter' is now total with type "set1 of set of A -> set of A".

possible side effects

Existing specifications that use 'set1' as an identifier would be invalidated.

A test suite for validation of the modification in the executable models (if appropriate).

None

[peterwvj]

We've decided to advance the RM. Tomohiro Oda has been appointed the owner.

[peterwvj]

We should keep in mind that this RM will affect PO generation. Also, I think this language change is equally relevant to VDM++ and VDM-RT.

[peterwvj]

Since VDM-10 already includes the seq1 type constructor, introducing set1 would be a natural extension to the language, I think.

Regarding the "possible side effects". I assume you mean set1'.

[paulch42]

@peterwvj Yes, my mistake. It should be 'set1' in 'possible side effects'. I corrected the proposal.

[ldcouto]

Honestly, I'm not sure I'm in favor of this. A user can create this type quite easily.

On the other hand, it's true that we have seq1 so you could make an argument for consistency. But we don't have map1 either so it's not a very strong argument...

[peterwvj]

I feel the same about it. Does anybody know why the seq1 type constructor was introduced into the language and the set1 (or map1) were not. Maybe @pglvdm or @nickbattle ?

[paulch42]

I did consider map1 though I have never had need of it and have never seen it in other specifications (admittedly not too many) so I didn't include it.

How does one define 'set1'? I am new to VDM so I want to define a type that says "set1 is a type of set with the invariant that values are non-empty". I want to say something like

set1[@a] = set of @a inv s1 == s1 <> {}

Maybe I am missing something obvious, but I can't see how to define a parameterised type in VDM. The left hand side of a type definition must be an identifier only.

[peterwvj]

The thing is that if you define it using a type definition you are limited to a particular element type. For example

types 
set1 = set of nat
inv xs == xs <> {};

Obviously you can use other types than nat, but it does not give you the flexibility of a set1 type constructor far as I can see. Type arguments (e.g. @T) only work for function as far as I am aware.

[pglvdm]

Hi all, Yes it is very easy to explain. In the old days (before the BSI and ISO standards) "seq of T" and "seq1 of T" was written as “T*" and "T+” as with regular expressions.

Cheers, Peter Peter Gorm Larsen Professor, PhD (head of software engineering) Telephone: +45 41 89 32 60 Mail: pgl@eng.au.dk Aarhus University, Department of Engineering, Finlandsgade 22, DK-8200 Aarhus N, Phone: +45 41893000

From: "Peter W. V. Tran-Jørgensen" notifications@github.com<mailto:notifications@github.com> Reply-To: overturetool/language reply@reply.github.com<mailto:reply@reply.github.com> Date: Tuesday 15 March 2016 at 10:12 To: overturetool/language language@noreply.github.com<mailto:language@noreply.github.com> Cc: Peter Gorm Larsen pgl@eng.au.dk<mailto:pgl@eng.au.dk> Subject: Re: [language] Request for Modification: set1 type (#35)

I feel the same about it. Does anybody know why the seq1 type constructor was introduced into the language and the set1 (or map1) were not. Maybe @pglvdmhttps://github.com/pglvdm or @nickbattlehttps://github.com/nickbattle ?

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub: https://github.com/overturetool/language/issues/35#issuecomment-196731846

[tomooda]

Apparently seq1 is used to type hd and tl operators. set1 will also make the type of the dinter operator a little cleaner.

Another place I might use set1 is to type functions that compute statistical properties, e.g. average, min, max and so on. They often assumes non emptiness. They can be of course specified in pre-conditions, but I feel emptiness is somewhat an essential property in set.

I don't have a particular example to use map1 type for now.

[paulch42]

If it was easy to define a generic set1 then it would be realistic to provide it as a library type. However, having to continually define specific set1 types is not particularly appealing. I would probably then simply stick with set and <>{} pre-conditions. In the end, my interest is in being able to create specifications that are as clear, concise and immediate as possible. I think set1 would aid in that. I view it as one of these "small difference individually, but significant impact globally" items.

[ldcouto]

You can use the wildcard operator to define non-empty sets of arbitrary types. But you can't parameterize those sets further so that's probably not what you want. I agree that set1 can improve readability of specifications.

Do we treat the type in the same was seq1 vis-à-vis type checking, proof obligations and execution?

[peterwvj]

@ldcouto I think that would be the most natural way to treat it.

[nickbattle]

Tomo, as owner of this, would you like to summarise what has been discussed so that we can quickly decide what to do at the meeting on Sunday?

[tomooda]

Summary of discussion so far

Discussion 1: Are there real needs? A non-empty set type can be defined as a set type using a type invariant.

• The type constructor set1 of will give more flexibility than the set of T inv s == s <> {} type.
• set1 of T, instead of set1 = set of ? inv s == s <> {}, will improve readability.

Discussion 2: Do we need map1 as well?

• No concrete example to use map1 type constructor was presented.

Discussion 3: What should be done to introduce set1?

• set1 should be added not only to VDM-SL but also to VDM++ and VDM-RT.
• Type checking and POG need to be extended in the same way as seq1.
• The type of dinter can be defined using set1 (need to modify type checker, POG and documentation).

[peterwvj]

The LB has decided to proceed with the RM, which enters the discussion phase.

[pglvdm]

I support this proposal since I also think that it would increase readability. On the other hand I would suggest not to introduce a map1 type constructor since then one would also need an inmap1 and it would give an unnecessary burden for newcomers to learn about so many possibilities.

[peterwvj]

The LB has decided to move this RM to 'Execution'.

[nickbattle]

I've made some updates to VDMJ to support set1. These can be tried from the link below. I will put this RM and RM36 into a new 3.2 release when they're both ready, but for now it's under a 3.1.1 release.

https://github.com/nickbattle/vdmj/releases/download/3.1.1-1/vdmj-3.1.1-RM35.jar

[nickbattle]

Consider the following two expressions, using the set1 type:

> p { x | x: set1 of bool }
= {{false, true}, {false}, {true}}

> p let s1:set1 of bool = {true, false} in power s1
= {{false, true}, {false}, {true}, {}}

The first enumerates all the members of the "set1 of bool" type, which therefore does not include the empty set. But the second one is taking the power set of a set1 of bool, which (currently) does include the empty set. So in a sense, the power operator is ignoring the fact that the set type passed as its argument cannot be empty.

Is that correct? :-)

[pglvdm]

I would certainly say that this is correct

[peterwvj]

I agree with PGL. The power operator is defined as "set of A ? set of set of A" so it does not

constrain the input in any way.

?

Both examples are correct IMHO.

PJ

---

From: Nick Battle notifications@github.com Sent: Thursday, June 30, 2016 14:17 To: overturetool/language Cc: Peter Würtz Vinther Tran-Jørgensen; Mention Subject: Re: [overturetool/language] Request for Modification: set1 type (#35)

Consider the following two expressions, using the set1 type:

p { x | x: set1 of bool } = {{false, true}, {false}, {true}}

p let s1:set1 of bool = {true, false} in power s1 = {{false, true}, {false}, {true}, {}}

The first enumerates all the members of the "set1 of bool" type, which therefore does not include the empty set. But the second one is taking the power set of a set1 of bool, which (currently) does include the empty set. So in a sense, the power operator is ignoring the fact that the set type passed as its argument cannot be empty.

Is that correct? :-)

You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/overturetool/language/issues/35#issuecomment-229641374, or mute the threadhttps://github.com/notifications/unsubscribe/AFI6d6g4RnINdIam1mqjM3W4W7Ux5lO_ks5qQ7PLgaJpZM4HvZVq.

[nickbattle]

This has now largely been ported over to Overture 2.3.9-SNAPSHOT. I've been testing some Jenkins builds, with the help of PJ, Paul and Tomo, but feel free to try yourselves.

See http://overture.au.dk/overture/test/Build-62_2016-07-20_14-45/

[nickbattle]

I've been adding the error message changes to this, and RM36, in the "editing" branch of the LRM, rather than creating new branches specifically for the two RMs. My expectation is that the LRM will be updated for both RMs in the editing branch as well, in anticipation of the next release.

There are still some more error message changes to make, but it shouldn't take long. I've generally taken the approach of changing existing messages to mention "in seq" or "in set" (say), where two error cases are the same, but for seq/set binds respectively, rather than creating separate new message numbers for each case.

[peterwvj]

I think that's fine! Thanks for doing this!

[peterwvj]

The feature proposed in this RM is available in Overture version 2.4.0 onwards, and the LRM has been updated accordingly.