Bug in sequence concatenation pattern

[joey-coleman]

The following bug was originally reported on Sourceforge by shinsahara, 2012-04-12 04:23:26:

I couldn't execute the following function. Overturetool stopped at line "[] -> v,": If I appended the line "[x] -> x," the I got the result. But, on VDMJ, VDMTools, and Overturetool 1.1.1 don't need the "[x] -> x," line. Other functional programming language like Haskell are same as {VDMJ, VDMTools, 1.1.1}.

public Foldr[@T1, @T2] : (@T1 -> @T2 -> @T2) -> @T2 -> seq of @T1 -> @T2 Foldr(f)(v)(s) == cases s : [] -> v, --[x] -> x, --I think I don't need to use this line, but I need on Overture Tool. On VDMJ and VDMTools, I don't need this line. [x]^xs -> f(x)(Foldr@T1,@T2(v)(xs)) end;

[joey-coleman]

Comment by shinsahara, 2012-04-12 04:23:27:

p new SequenceF().run()> Files were attached:

• SequenceF.vdmpp (942 bytes)

[joey-coleman]

Comment by nick_battle, 2012-04-12 06:40:27:

It looks like this was a deliberate change introduced recently in Overture to make it the same as VDMTools, in particular to mean that sequence concatenation does not match an empty sequence in its left or right part (eg. a ^ b cannot match a sequence with one item). Before the recent change, you could match an empty item in a concatenation.

I made the change after consultation with Peter.

[joey-coleman]

Comment by shinsahara, 2012-04-13 05:32:53:

Dr. Kei Sato (who is the maintainer of the VDMTools) said that "xs" can be empty in "[x]^xs" expression. The opinion is based on the VDM-SL specification of the VDMTools interpreter. From VDM Language Manual, we feel "xs" is not empty. But, the representation of the manual is ambiguous. So, I think xs = [ ] is OK.

[joey-coleman]

Comment by nick_battle, 2012-07-11 12:22:33.628000:

I think this has been "fixed" (ie. changed back). VDMJ will now match empty sequences in a concatenation, but only as a last resort if there are no other non-empty matches.

• status: open --> closed