Append map pattern

[joey-coleman]

The following bug was originally reported on Sourceforge by shinsahara, 2011-11-16 06:02:18:

1. Identification of the Originator: Dr. Kei Sato (SCSK Corporation)
2. Target of the request: To use in code conversion. And, we've already used "map pattern" in code conversion on VDMTools.
3. Motivation for the request: Convenient to write clear specification.
4. Description of the request: (a) description of the modification: map enum pattern = '{', maplet pattern list, '}'; maplet pattern list = maplet pattern, { ',', maplet pattern }; maplet pattern = pattern, '|->', pattern;

map override pattern = pattern, '++', pattern;

A map enumeration pattern fits only map values. The maplet patterns are matched to distinct elements of a map; all elements must be matched.

A map override pattern fits only map values. The two patterns are matched to a partition of two sub maps of a map. In the Toolbox the two sub maps will always be chosen such that they are non-empty and disjoint.

(b) benefits from the modification: Same as 3. (c) possible side effects: Probably, side effects occur on Proof

1. sample test suite:

d let { 1 |-> a } = { 1 |-> 2 } in a 2

d let { 1 |-> a, a |-> b, b |-> c } = { 1 |-> 4, 2 |-> 3, 4 |-> 2 } in c 3

d { a | { 1 |-> a } ++ - in set { { 1 |-> 2, 3 |-> 5, 6 |-> 'a' } } } { 2 }

[joey-coleman]

Comment by nick_battle, 2011-11-18 12:27:08:

This is an interesting proposal. What would happen with pattern bindings where there is an ambiguity in the map's domain, like "let {a |-> 2} = {1 |-> 2, 2 |-> 2} in a"? I suppose that would be a new case of looseness ("a" could be 1 or 2)? And so in expressions where all possibilities are considered (like exists and forall), all bindings would be tested?

[joey-coleman]

Comment by shinsahara, 2011-11-20 03:54:01:

"let {a |-> 2} = {1 |-> 2, 2 |-> 2} in a" becomes run-time error. This is same as "let {a} = {1,2} in a"

"let { a |-> 2, b |-> 2 } = {1 |-> 2, 2 |-> 2} in a" => (a= 1, b=2) or (a = 2 or b = 1)

[joey-coleman]

Comment by shinsahara, 2012-02-01 04:36:33:

specification of map pattern

Files were attached:

• MapPattern.rtf (13917 bytes)

[joey-coleman]

Comment by nick_battle, 2012-02-01 09:07:47:

Presumably the map override pattern is trying to provide the same "partitioning" ability as the sequence concatenation and set union patterns? So why isn't it a "munion" pattern? The ++ override implies that the RHS can replace domain items on the LHS, but munion does not (overlaps are an error).

[joey-coleman]

Comment by shinsahara, 2012-02-02 02:05:16:

Dr.k thinks "++" is shorter than "munion" :-) And, following are same effect and meaning, because RHS should be a map. let m1 munion m2 = aMap in ... let m1 ++ m2 = aMap in ...

[joey-coleman]

Comment by nick_battle, 2012-02-02 08:02:04:

Well, I agree it's shorter(!), but intuitively the ++ override operator has the wrong semantic implication. The LHS and RHS are not chosen so that m1 ++ m2 = m after the match, they are chosen so that m1 munion m2 = m, surely? (I agree the result would be the same, but you see my point? ++ and munion mean different things).

[joey-coleman]

Comment by shinsahara, 2012-02-06 02:32:07:

Dr.k was persuaded to "++" -> "munion".

So, map merge pattern = pattern, 'munion', pattern;

[joey-coleman]

Comment by nick_battle, 2012-04-16 17:47:32:

Should the maplet pattern list allow the empty map to be defined? Comparing this to set enum and sequence enum patterns, you ought to be able to match against the empty map as you can with the empty sequence and set. Do you agree (and does the VDMTools implementation do this?)

map enum pattern = '{', maplet pattern list, '}' | ' {', '|->', '}';

[joey-coleman]

Comment by shinsahara, 2012-04-17 01:46:27:

Dr. Kei Sato and I agree following:

map enum pattern = '{', maplet pattern list, '}' | ' {', '|->', '}';

[joey-coleman]

Comment by sunewolff, 2012-09-07 08:24:36.580000:

• no: --> 3438625
• milestone: --> Discussion

[joey-coleman]

Comment by sunewolff, 2012-09-07 08:35:51.174000:

• vdmtools_implementation: --> Available in 9.0
• vdmj_implementation: -->

[joey-coleman]

Comment by sunewolff, 2012-09-07 08:40:54.657000:

• assigned_to: Shin Sahara

[joey-coleman]

Comment by nick_battle, 2012-09-09 11:56:13.515000:

• lrm_updated: --> False
• vdmj_implementation: --> Available in 1.2.1
• milestone: Discussion --> Execution

[joey-coleman]

Comment by shinsahara, 2012-10-14 08:42:35.056000:

I've modified "++" to minion.

1. Identification of the Originator: Dr. Kei Sato (SCSK Corporation)
2. Target of the request: To use in code conversion. And, we've already used "map pattern" in code conversion on VDMTools.
3. Motivation for the request: Convenient to write clear specification
4. Description of the request:
   • description of the modification:
     • map enum pattern = '{', maplet pattern list, '}';
     • maplet pattern list = maplet pattern, { ',', maplet pattern };
     • maplet pattern = pattern, '|->', pattern;
     • map muinon pattern = pattern, 'munion', pattern;
     • A map enumeration pattern fits only map values. The maplet patterns are matched to distinct elements of a map; all elements must be matched.
     • A map munion pattern fits only map values. The two patterns are matched to a partition of two sub maps of a map.
     • In the Toolbox the two sub maps will always be chosen such that they are non-empty and disjoint.
   • benefits from the modification: Same as 3.
   • possible side effects: Probably, side effects occur on Proof
   • sample test suite:
     • d let { 1 |-> a } = { 1 |-> 2 } in a = 2
     • d let { 1 |-> a, a |-> b, b |-> c } = { 1 |-> 4, 2 |-> 3, 4 |-> 2 } in c = 3
     • d { a | { 1 |-> a } munion - in set { { 1 |-> 2, 3 |-> 5, 6 |-> 'a' } } } = { 2 }

[joey-coleman]

Comment by sunewolff, 2012-11-13 09:10:23.262000:

• status: open --> closed
• lrm_updated: False --> True

[joey-coleman]

Comment by sunewolff, 2012-11-13 09:11:23.659000:

• milestone: Execution --> COMPLETED

[joey-coleman]

implemented in overturetool/overture@0b89dbb5b34ff45aabb6064fd6b839dd0aeb3020