// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // This Quartz file can be used to test the parser and type-checker for tools // // using the Quartz language. // // ************************************************************************** // macro minmax(x,y) = ((x<y)?(x,y):(y,x)); module Expressions( bool xbl,ybl,zbl, bv{1} xbv1,ybv1,zbv1, bv{4} xbv4,ybv4,zbv4, bv{12} xbv,ybv,zbv, nat{4} xn4,yn4,zn4, int{4} xi4,yi4,zi4, nat xn,yn,zn, int xi,yi,zi, real xr,yr,zr, (int * int) t, [4]bool xa ) { // ---- boolean constants xbl = instant; xbl = inside; xbl = terminate; xbl = true; xbl = false; xbv1 = true; xbv1 = xbl; // ---- bitvector constants xbv = 0b101011110000; xbv = 0o1752; xbv = 0xAFD; // ---- nat constants xn = 3; // ---- int constants xi = 3; xi = +3; xi = -3; // ---- real constants xr = 0.23; xr = +0.23; xr = -424.43243; xr = 3213.4324e-12; xr = 3213.4324e+12; xr = +3213.4324e-12; xr = +3213.4324e+12; xr = -3213.4324e-12; xr = -3213.4324e+12; // ---- (bitwise) boolean boperators zbl = !ybl; zbl = xbl & ybl; zbl = xbl | ybl; zbl = xbl -> ybl; zbl = xbl <-> ybl; zbv = !ybv; zbv = xbv & ybv; zbv = xbv | ybv; zbv = xbv -> ybv; zbv = xbv <-> ybv; zbv1 = !ybl; zbv1 = xbv1 & ybl; zbv1 = xbv1 | ybl; zbv1 = xbv1 -> ybl; zbv1 = xbv1 <-> ybl; zbl = !ybl; zbl = xbv1 & ybl; zbl = xbv1 | ybl; zbl = xbv1 -> ybl; zbl = xbv1 <-> ybl; // ---- equalities and inequalities zbl = (xbl == ybl); zbl = (xbv == ybv); zbl = (xbl == ybv1); zbl = (xn == yn); zbl = (xi == yi); zbl = (xi == yn); zbl = (xr == yr); zbl = (xbl != ybl); zbl = (xbv != ybv); zbl = (xbl != ybv1); zbl = (xn != yn); zbl = (xi != yi); zbl = (xi != yn); zbl = (xr != yr); // ---- arithmetic operators zn = xn + yn; zn = xn - yn; zn = xn * yn; zn = xn / yn; zn = xn % yn; zi = xi + yi; zi = xi - yi; zi = xi * yi; zi = xi / yi; zi = xi % yi; zi = xn + yi; zi = xn - yi; zi = xn * yi; zi = xn / yi; zi = xn % yi; zi = xi + yn; zi = xi - yn; zi = xi * yn; zi = xi / yn; zi = xi % yn; // ---- special arithmetic operators zn = abs(xi); zn = sat{3}(xn); // zi = sat{4}(xi+yi); // ---- bitvector operators zbl = xbv{2}; // bit access zbv = xbv4@ybv4@zbv4; // bitvector append zbv4 = xbv{5:2}; // bitvector segment extraction zbv4 = xbv{-2:7}; // bitvector segment extraction zbv4 = xbv{-2:-5}; // bitvector segment extraction zbv4 = xbv{10:-5}; // bitvector segment extraction zbv = reverse(xbv); // reverse of bitvector zbv4 = {xbl::4}; // replicating a boolean // ---- tuple expressions t = minmax(xn,yn); t = (t.1,t.0); t.1 = xn+yn; xn = t.1 + t.0 + (minmax(xn,yn)).0; t = (xn,yn); // ------- explicit type converters -------------------------- zbv1 = xbl; // bool2bv is inserted by type-checker zbv4 = nat2bv(xn4,2)@nat2bv(yn4,2); zbv4 = int2bv(xn4,3)@xbl; zbv4 = arr2bv(xa); zbv4 = tup2bv((xbl,ybl,zbl,xbl)); // tup2bv required double delimiters zn4 = bv2nat(xbv4); // generates assertion bv2nat(xbv4)<4 zi4 = bv2int(xbv4); // generates assertion bv2int(xbv4)<4 & -4<=bv2int(xbv4) zn4 = bv2int(xbv4); // generates assertion bv2int(xbv4)<4 & 0<=bv2int(xbv4) zr = nat2real(xn); zr = int2real(xi); // ------- special real-expressions -------------------------- zr = cos(xr) + sin(yr); zr = exp(xr,yr); zr = log(xr); zr = drv(yr); }