Homework: Reading Formal Contract Specifications

1. Add a recent, clear photo of yourself to both your Zoom profile and to your Carmen profile. (Nothing to turn in for this question)

2. Consider the following contract specification for the static method smooth.

   /**
    * No informal description here for obvious reasons...
    *
    * @replaces s2
    * @requires |s1| >= 1
    * @ensures <pre>
    * |s2| = |s1| - 1  and
    *  for all i, j: integer, a, b: string of integer
    *      where (s1 = a * <i> * <j> * b)
    *    (there exists c, d: string of integer
    *       (|c| = |a|  and
    *        s2 = c * <(i+j)/2> * d))
    * </pre>
    */
   public static void smooth(Sequence<Integer> s1, Sequence<Integer> s2) {...}
   

   Answer the following questions.

   1. Suppose seq1 = < 2, 4, 6 >, seq2 = < -5, 12 >. What are the values of seq1 and seq2 after the call smooth(seq1, seq2)?
   2. Suppose seq1 = < 7 >, seq2 = < 13, 17, 11 >. What are the values of seq1 and seq2 after the call smooth(seq1, seq2)?
   3. Suppose seq1 = < >, seq2 = < >. What are the values of seq1 and seq2 after the call smooth(seq1, seq2)?
   4. Explain informally, but precisely, what the specs of smooth say about the method's behavior. In other words, explain in English what smooth is supposed to do.