Changed behaviour of ADTs (bags, seq)

[sakehl]

//:: cases axiomatic-data-types-bag-constructing-bags-from-existing-bags-1
//:: verdict Pass
//:: tools silicon
class Test {
    void test() {
        bag<int> b9 = bag<int> { 3 };
        bag<int> b10 = bag<int> { 3, 4 };
        bag<int> b11 = bag<int> { 1, 2, 2, 3 };
        bag<int> b12 = bag<int> { 2, 3, 3, 4 };
        bag<int> b13 = bag<int> { 1, 1, 2, 3 };
        bag<int> b14 = bag<int> { 2, 3, 3, 4 };
        
        assert b9 + b10 == bag<int> { 3, 3, 4 };
        assert b12 - b11 == bag<int> { 3, 4 };
        assert b11 - b12 == bag<int> { 1, 2 };
        assert b13 * b14 == bag<int> { 2, 3 };
        
    }
}

This code from the website does not pass anymore
It gives

At axiomatic-data-types-bag-constructing-bags-from-existing-bags-1.pvl
--------------------------------------
   14          assert b12 - b11 == bag<int> { 3, 4 };
   15          assert b11 - b12 == bag<int> { 1, 2 };
                     [---------
   16          assert b13 * b14 == bag<int> { 2, 3 };
                      ---------]
   17          
   18      }
--------------------------------------
Expected types to numeric, but got: bag<int> and bag<int>

So probably ambigous mult, or type coercion is not working as expected anymore.

[sakehl]

For seqs this does not work anymore:

//:: cases axiomatic-data-types-sequence-examples-distinct-element-1
//:: verdict Pass
//:: tools silicon
class Test {
    pure boolean distinct(seq<int> s) =
        (\forall int i; 0 <= i && i < s.length; 
            (\forall int j; 0 <= j && j < s.length && s[i] == s[j]; i == j)
        );
    
}

At axiomatic-data-types-sequence-examples-distinct-element-1.pvl

4  class Test {
5      pure boolean distinct(seq<int> s) =
                                        [--------
6          (\forall int i; 0 <= i && i < s.length; 
                                         --------]
7              (\forall int j; 0 <= j && j < s.length && s[i] == s[j]; i == j)
8          );

---

Could not find field named length.

[sakehl]

class SetComp {
    requires 0 <= j && j < 5;
    void myMethod(int j) {
       set<int> a = set<int> {SetComp.plus(x, x) | int x; x >= 0 && x <= 5 };
       assert plus(1, 1) in a; 
       assert plus(j, j) in a; 
    }

    pure static int plus(int a, int b) = a+b;
}

This example from the tutorial.

Set comprehension is on the website, but we do not support this anymore? Also the example does not verify on the website? So maybe remove it?

At axiomatic-data-types-set-set-comprehension-1.pvl
--------------------------------------
    5      requires 0 <= j && j < 5;
    6      void myMethod(int j) {
                          [--------------------------------------------------------
    7         set<int> a = set<int> {SetComp.plus(x, x) | int x; x >= 0 && x <= 5 };
                           --------------------------------------------------------]
    8         assert plus(1, 1) in a; 
    9         assert plus(j, j) in a;
--------------------------------------
Parsing failed: This construct (ValSetComprehensionContext) is syntactically valid, but not supported by VerCors.

All other examples on the website do not seem to be working as well. Although they mostly run fine on latest dev.

[superaxander]

I did add a note a couple of months ago that we don't support set comprehensions at the moment, but the change seems to have not appeared on the website, not sure why.

[sakehl]

Ah yes it is there! I just missed it