This verification example contains summations (i.e. the use of "\sum" expressions) over sequences of floats. Both passing and failing cases are included.
xxxxxxxxxx
// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases TestFloat
// tools silicon
// verdict Pass TestFloat.main TestFloat.add TestFloat.prefixsum
class TestFloat {
public static void main(String args[]){
float a,b,c,d;
a=(float)1;
b=(float)2;
c=a+b;
d=b+a;
//@ assert c == d;
/*@
seq<float> s=seq<float>{};