class Adder {
    public static void test(boolean a, boolean b, boolean c)
    /*@test_pre@*/
    {
        boolean s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13;
        boolean z, cn;
	                         // fff fft ftf ftt tff tft ttf ttt 
                                 //---------------------------------
        s1 = and(b,c);           //  f   f   f   t   f   f   f   t
        s2 = and(a,c);           //  f   f   f   f   f   t   f   t
        s3 = and(a,b);           //  f   f   f   f   f   f   t   t
        s4 = or(s1,s2);          //  f   f   f   t   f   t   f   t
        cn = or(s3,s4);          //  f   f   f   t   f   t   t   t

        s5 = not(a);             //  t   t   t   t   f   f   f   f
        s6 = not(b);             // f/t f/t t/f t/f f/t f/t  f   f 
//      s6 = and(b,s5);     
        s7 = not(b);             //  t   t   f   f   t   t   f   f
        s8 = and(a,s7);          //  f   f   f   f   t   t   f   f
        s9 = or(s6,s8);          // f/t f/t t/f t/f  t   t   f   f

        s10 = not(s9);           // t/f t/f f/t f/t  f   f   t   t
        s11 = and(c,s10);        //  f  t/f  f  f/t  f   f   f   t
        s12 = not(c);            //  t   f   t   f   t   f   t   f
        s13 = and(s9,s12);       // f/t  f  t/f  f   t   f   f   f
        z = or(s11,s13);         // f/t t/f t/f f/t  t   f   f   t
	                         // correct/computed
    }
    /*@test_post@*/
                                 // Number of Diags: [stmt] [%] [expr] [%]
                                 //----------------------------------------
                                 //  *                  10  33     16   27
                                 //      *              14  47     22   37
                                 //          *          12  40     19   32
                                 //              *      12  40     19   32
                                 //  *   *              10  33     15   25
                                 //  *       *           8  27     12   20
                                 //  *           *       6  20      8   13
                                 //      *   *          10  33     14   23
                                 //      *       *      10  33     15   25
                                 //          *   *      10  33     15   25
                                 //  *   *   *           8  27     11   18
                                 //  *   *       *       6  20      8   13
                                 //  *       *   *       6  20      8   13
                                 //      *   *   *       8  27     11   18
                                 //  *   *   *   *       6  20      8   13
    
    static boolean not(boolean x)
    {
        return !x;
    }
    
    static boolean and(boolean x, boolean y)
    {
        return x && y;
    }
    
    static boolean or(boolean x, boolean y)
    {
        return x || y;
    }
}