Missing support for \sum

[ArmborstL]

I tried to use the (\sum type name; expr; expr) syntax in specifications inside a java file;

public void example6(int x, seq<int> s) {
  //@ assert x == (\sum int i; 0<i && i<|s|; s[i]*s[i]);
}

Viper does not seem to support the translated version of the \sum command:

[progress] verifying with builtin silicon backend
[abort] binder Sum not supported
[debug] At Main.java:657:
The final verdict is Error

I suppose \sum should either be removed from the parser (together with #453), or translated into a different Viper expression.

[OmerSakar]

I remember this working and as mentioned I looked into this.

If we look at the example (in the example directory) basic/sumints.pvl, we see how the \sum binder is meant to be used. https://github.com/utwente-fmt/vercors/blob/b8a5a6e8767321e2a107fd45482ac502752f4fde/examples/basic/sumints.pvl#L9-L16

Here we sum over a sequence and just say xs[i] for a certain range. This goes through the pass "simplify_sums" that uses jspec to rewrite this form into a form like "sum this sequence over this range" (see below). That form of the sum binder does have a mapping in Viper, namely through the StandardOperator FoldPlus.

https://github.com/utwente-fmt/vercors/blob/b8a5a6e8767321e2a107fd45482ac502752f4fde/src/main/universal/res/config/summation.jspec#L11-L15

Workaround

The obvious workaround is to create a function that does the squaring and use the sum binder (see example below).

class SumSeqOfInts {

    ensures |xs| == |\result|;
    ensures (\forall int i; 0 <= i && i < |\result|; \result[i] == (xs[i]*xs[i]));
    pure seq<int> sqr(seq<int> xs) =
        |xs| == 0 ?
            [t:int] :
            ((head(xs)*head(xs)) :: sqr(tail(xs)))
    ;

    void main() {
        seq<int> xs = seq<int> {1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
        assert (\sum int k; 0 <= k && k < |xs|; xs[k]) == 55;

        seq<int> sqrxs = sqr(xs);
        assert (\sum int k; 0 <= k && k < |sqrxs|; sqrxs[k]) == 385; 
    }
}

Discussion points

I think the question now is not whether to remove it from the syntax (since there is support for it in the form described above). I think the question now is whether we want the sum binder to work as suggested in the issue.

The sum binder works in Viper as follows. The sequence is transformed into a VectorExpression (a domain we made, see prelude.sil) and the function vsum is defined (with accompanying axioms) over a VectorExpression given a certain range. This function vsum is our sum binder. It is (currently) not possible to say that we want to sum the squares of the elements of a sequence (i.e. xs[i]*xs[i]). I do not think it is possible to support this using the vsum function or a domain function.