int W;
W = 20;

int scasize(int [] str) {
    return 0;
}

boolean scnewline(int ch) {
    return true;
}

boolean scblank(int ch) { 
    return true;
}

boolean scalpha(int ch) { 
    return true;
}

boolean scnum(int ch) { 
    return true;
}

boolean scalphanum(int ch) { 
    return true;
}

//////////////////////////////////////////////////
boolean scaempty(int [] str) {
    return scasize(str) == 0;
}

boolean scaequal(int [] s1, int [] s2) {
    int i;
    int r;
    r = scasize(s1);
    if (r != scasize(s2))
        return false;
    i = 0;
    while (i < r) {
        if (s1[i] != s2[i])
            return false;
        i = i+1;
    }
    return true;
}

boolean scasubeq(int[] s1,int l1,int r1,int [] s2,int l2, int r2) {
    int i1;
    int i2;
    if (r1-l1 != r2-l2)
        return false;
    i1 = l1;
    i2 = l2;
    while( i1 <= r1) {
        if (s1[i1] != s2[i2])
            return false;
        i1 = i1 + 1;
        i2 = i2 + 1;
    }
    return true;
}
//////////////////////////////////////////////////


boolean blank(int [] str) {
    @pre blankSpec {
        true;
    }
  return ( scasize(str) > 0) && 
      (forall (int k:[0 .. scasize(str) - 1] ) { scblank( (str[k]))});
    @post blankSpec {
      scasize(str) > 0;
      forall (int k:[0 .. scasize(str) - 1] ) { scblank( (str[k]))};
    }

    @behavior blankSpec {
        good {input={str="  "}; output={rv=true}};
        good {input={str=""}; output={rv=false}};
        bad  {input={str=""}; output={rv=true}};
        good {input={str=" a"}; output={rv=false}};
    }
}

boolean subIsBlank(int [] str, int l, int r) {
    @pre subIsBlankSpec { 
        0 <= l <= r < scasize(str); }
  return (0 <= l <= r < scasize(str)) &&
      (forall (int k:[l .. r] ) { scblank( (str[k]))});
  @post subIsBlankSpec { 
      0 <= l <= r < scasize(str);
      forall (int k:[l .. r] ) { scblank( (str[k]))};
  }
  @behavior subIsBlankSpec {
     good {input={str="  ",l=0,r=1}; output={rv=true}};
     good {input={str="",l=0,r=0}; output={rv=false}};
     bad  {input={str="",l=0,r=0}; output={rv=true}};
     good {input={str=" a",l=0,r=1}; output={rv=false}};
  }
}

boolean subIsBlankOrNewline(int [] str, int l, int r) {
    @pre subIsBNLSpec { 
        0 <= l <= r < scasize(str); }
  return (0 <= l && l <= r && r < scasize(str)) &&
      (forall (int k:[l .. r] ) { scnewline((str[k])) || scblank((str[k]))});
  @post subIsBNLSpec { 0 <= l <= r < scasize(str);
      forall (int k:[l .. r] ) { scnewline((str[k])) || scblank((str[k]))};
  }
  @behavior subIsBlankSpec {
     good {input={str="  N",l=0,r=1}; output={rv=true}};
     good {input={str="N ",l=0,r=1}; output={rv=true}};
     good {input={str="N",l=0,r=0}; output={rv=true}};
     good {input={str="  ",l=0,r=1}; output={rv=true}};
     good {input={str="",l=0,r=0}; output={rv=false}};
     bad  {input={str="",l=0,r=0}; output={rv=true}};
     good {input={str=" a",l=0,r=1}; output={rv=false}}; }
}

boolean subIsWord(int [] str, int l, int r) {
  @pre subIsWSpec { 
        0 <= l <= r < scasize(str); }
  return (0 <= l && l <= r && r < scasize(str)) &&
      (r - l - 1 < W/2) &&
      (forall (int k:[l .. r] ) { scalphanum( (str[k]))});
  @post subIsWSpec { 0 <= l <= r < scasize(str);
      r - l - 1 < W/2;
      forall (int k:[l .. r] ) { scalphanum( (str[k]))};}
  @behavior subIsWSpec {
     good {input={str=" aaa ",l=1,r=3}; output={rv=true}};
     good {input={str=" aaa ",l=0,r=3}; output={rv=false}};
     good {input={str="  ",l=0,r=1}; output={rv=false}};
     good {input={str=" aaN",l=1,r=3}; output={rv=false}};
     good {input={str=" aaN",l=1,r=3}; output={rv=true}}; }
}

boolean word(int [] str) {
  @pre wSpec { true;}
  return subIsWord(str, 0, (scasize(str) - 1));
  @post wSpec { 
      forall (int k:[0 .. scasize(str) - 1] ) { scalphanum( (str[k]))};}
  @behavior wSpec {
     good {input={str=" aaa "}; output={rv=true}};
     good {input={str=" aaa "}; output={rv=false}};
     good {input={str="  "}; output={rv=false}};
     good {input={str=" aaN"}; output={rv=false}};
     good {input={str=" aaN"}; output={rv=true}}; }
}

boolean subIsLine(int [] str, int l, int r) {
  @pre subIsLSpec { 
        0 <= l <= r < scasize(str); }
  return  
      ( (0 <= l && l <= r && r < scasize(str)) &&
        (subIsWord(str,l,(r-1)) && scnewline((str[r])) ) ) &&
      ( exists (int k:[l .. r] ) { 
        subIsWord(str,l,k) && scblank((str[k])) && subIsLine(str,(k+1),r)});
  @post subIsLSpec {
      0 <= l <= r < scasize(str);
      subIsWord(str,l,(r-1));
      scnewline((str[r]));
      exists (int k:[l .. r] ) { 
        subIsWord(str,l,k) && scblank((str[k])) && subIsLine(str,(k+1),r) };
  }
  @behavior subIsLSpec {
     good {input={str=" aaaN",l=1,r=4}; output={rv=true}};
     good {input={str=" aaaN",l=0,r=4}; output={rv=false}};
     good {input={str="   ",l=0,r=3}; output={rv=false}};
     good {input={str=" aa aaaN",l=1,r=7}; output={rv=true}};
     bad  {input={str=" aa aaaN",l=1,r=7}; output={rv=false}};
     bad  {input={str=" aa aa N",l=1,r=3}; output={rv=true}};
     bad  {input={str=" aaNaa N",l=0,r=2}; output={rv=true}};
  }
}

boolean line(int [] str) {
  @pre lSpec { true;}
    return subIsLine(str, 0, (scasize(str) - 1));
  @post lSpec {
        subIsWord(str,0, (scasize(str) - 1));
        scnewline((str[scasize(str) - 1]));
      exists (int k:[0 .. scasize(str) - 1] ) { 
        subIsWord(str,0,k) && scblank((str[k])) && 
        subIsLine(str,(k+1),(scasize(str) - 1)) };
    }
  @behavior subIsLSpec {
     good {input={str="aa aaN"}; output={rv=true}};
     good {input={str=" aaaN"}; output={rv=false}};
     good {input={str="   "}; output={rv=false}};
     good {input={str="aa aaaN"}; output={rv=true}};
     bad  {input={str="aa aaaN"}; output={rv=false}};
     bad  {input={str="aa "}; output={rv=true}};
     bad  {input={str=" aa"}; output={rv=true}};
  }
}

boolean subIsPara(int [] str, int l, int r) {
  @pre subIsPSpec { 
        0 <= l <= r < scasize(str); }
    return subIsLine(str,l,r) ||
        (exists (int k:[l .. r]) {  subIsLine(str,l,k) && subIsPara(str, (k+1), r)});
  @post subIsPSpec {
      0 <= l <= r < scasize(str); 
      subIsLine(str,l,r) ||
        (exists (int k:[l .. r]) {  subIsLine(str,l,k) && subIsPara(str, (k+1), r)});
  }
  @behavior subIsPSpec {
     good {input={str="aa aaN",l=0,r=5}; output={rv=true}};
     good {input={str="aa aaNaaa aaaN",l=0,r=13}; output={rv=true}};
     good {input={str="aa   aaNaaa   aaaN",l=0,r=17}; output={rv=true}}; // multi-blanks are fine
     good {input={str="aa aaNaaa aaaN",l=2,r=13}; output={rv=false}};//para does not start with a space
     bad  {input={str=" aaa ",l=1,r=4}; output={rv=true}};
  }
}

boolean para(int [] str) {
  @pre paraSpec { true;}
    return subIsPara(str,0, (scasize(str) - 1));
  @post paraSpec {
      subIsLine(str,0,(scasize(str) - 1)) ||
          (exists (int k:[0 .. (scasize(str) - 1)]) {
            subIsLine(str,0,k) && 
            subIsPara(str,(k+1),(scasize(str) - 1))});
  }
  @behavior paraSpec {
     good {input={str="aa aaN"}; output={rv=true}};
     good {input={str="aa aaNaaa aaaN"}; output={rv=true}};
     good {input={str="aa   aaNaaa   aaaN"}; output={rv=true}}; // multi-blanks are fine
     good {input={str=" aaNaaa aaaN"}; output={rv=false}};//para does not start with a space
     bad  {input={str="aaa "}; output={rv=true}};
     }
}

boolean headTailOfSub(int [] str, int l, int w, int k) {
    @pre subHTSpec {
        subIsPara(str,l,(scasize(str) -1));// str[l,|str|-1] is a paragraph
        0 <= l < w <= k < scasize(str);
    }
    return subIsWord(str,l,w) &&
        ( (scnewline((str[w+1])) && scasize(str) == (w+2) ) ||
          ( subIsBlankOrNewline(str,(w+1),k) && 
            subIsPara(str,(k+1),(scasize(str)-1) )
          ));
    @post subHTSpec {
        subIsPara(str,l,(scasize(str) -1)); 
        0 <= l < w <= k < scasize(str);
        (scnewline((str[w+1])) && scasize(str) == (w+2) ) || //para=word-newline
          ( subIsBlankOrNewline(str,(w+1),k) &&      //para=word-blank|newline-para
            subIsPara(str,(k+1),(scasize(str)-1) )); //     l  w             k
    }
    @behavior subHTSpec {
     good {input={str="aa  aaN",l=0,w=1,k=4}; output={rv=true}};
     good {input={str="aa  aaN aaaaaN",l=0,w=1,k=4}; output={rv=true}};
     bad  {input={str="aa  aaN aaaaaN",l=0,w=1,k=3}; output={rv=true}};
     good {input={str="aa  aaN aaaaaN",l=0,w=1,k=3}; output={rv=false}};
     good {input={str="aa  aaN",l=1,w=1,k=4}; output={rv=true}};
     good {input={str="aa  aaN aaaaaN",l=1,w=1,k=4}; output={rv=true}};
     }
}

int headSub (int [] str, int l) {
    int i;
    int ch;
    int r;

    @pre hdSpec { subIsPara(str,l,(scasize(str) -1));}

    // the first character is guaranteed to be alphanum since str is a paragraph
    ch = str[l];
    i = l+1;
    r = scasize(str);

    while (i < r) {
        ch = str[i];
        if (scblank(ch) || scnewline(ch)){
            return i-1;
        }
    }
    return -1;// this should never happen

    @post hdSpec {
        scnewline((str[rv+1])) ||
        (exists (int k:[rv+1 .. scasize(str) - 1]){ 
           headTailOfSub(str, l, rv, k) 
         });
    }
}

int tailSub(int [] str, int l, int hd) {
    int ch;
    int i;
    int r;
    @pre tlSpec { 
        subIsPara(str,l,(scasize(str) -1));
    }
    r = scasize(str);
    i = hd+1;
    while (i < r) {
        ch = str[i];
        if ((scalphanum(ch))){
            return i;
        }
    }
    return -1;
    @post tlSpec {
        (rv != -1) -> headTailOfSub(str,l,hd,rv);
    }
}

boolean isMinSeparationBool (int [] str, int l, int min, boolean b) {
    return
        (subIsWord(str, l, (scasize(str) - 2) ) && 
          scnewline((str[(scasize(str) -1)])) && 
          min == 1000) 
      ||
        (exists (int k:[l+1 .. (scasize(str) -1)]) { 
         exists (int m:[k+1 .. (scasize(str) -1)]) {
            subIsWord (str, l, (k-1)) &&
            subIsBlank(str, k, (m-1)) && 
            subIsLine(str, m, (scasize(str) -1)) &&
            ( exists (boolean isMin) {
              min <= (m-k) && isMinSeparationBool(str, m, min, isMin)  &&
              (b == (min == (m-k))) &&
              ((min == (m - k)) || isMin)
              }) } } );
}

boolean isMinSeparation(int [] str, int l, int min) {
    return isMinSeparationBool(str, l, min, true) ||
        isMinSeparationBool(str, l, min, false);
}

boolean isMaxSeparationBool(int [] str, int l, int max, boolean b) {
    return
        (subIsWord(str, l, (scasize(str) - 2) ) && 
          scnewline((str[(scasize(str) -1)])) && 
          max == -1) 
      ||
        (exists (int k:[l+1 .. (scasize(str) -1)]) { 
         exists (int m:[k+1 .. (scasize(str) -1)]) {
            subIsWord (str, l, (k-1)) &&
            subIsBlank(str, k, (m-1)) && 
            subIsLine(str, m, (scasize(str) -1)) &&
            ( exists (boolean isMax) {
              max <= (m-k) && isMaxSeparationBool(str, m, max, isMax)  &&
              (b == (max == (m-k))) &&
              ((max == (m - k)) || isMax)
              }) } } );
}

boolean isMaxSeparation(int [] str, int l, int max) {
    return isMaxSeparationBool(str, l, max, true) ||
        isMaxSeparationBool(str, l, max, false);
}

int minSeparation (int [] str, int l) {
    int ch;
    int i;
    int j;
    int sep;
    int minSubSep;
    int min;
    @pre minSpSpec {
        line (str);
    }

    //the base case happens when str[l:|str|-1] = word-N
    if (subIsWord(str, l, (scasize(str) - 2) ) ) {
        return 1000;//infinity
    }

    i  = 0;
    ch = str[0];
    while (!scblank(ch)) {
        i = i+1;
        ch = str[i];
    }
    // i here is the first blank after l
    j = i+1;
    ch = str[j];
    while (scblank(ch)) {
        j = j+1;
        ch = str[j];
    }
    // j here is the first non-blank after i
    sep = j - i; 
    minSubSep = minSeparation(str, j);
    if (minSubSep < sep ){
        min = minSubSep;
    } else { 
        min = sep;
    }
    return  min;

    @post minSpSpec {
        isMinSeparation (str, 0, rv) ;
    }
    @behavior minSpSpec {
        good {input={str="aaN",l=0};
              output={rv=1000}};
        bad {input={str="aaN",l=0};
              output={rv=0}};
        good {input={str="aa aa  aaa aaN",l=0};
              output={rv=1}};
        bad {input={str="aa aa  aaa aaN",l=0};
              output={rv=2}};
        bad {input={str="aa  aa   aaa  aaN",l=0};
              output={rv=1}};
    }
}

int maxSeparation (int [] str, int l) {
    int ch;
    int i;
    int j;
    int sep;
    int maxSubSep;
    int max;
    @pre maxSpSpec {
        line (str);
    }

    //the base case happens when str[l:|str|-1] = word-N
    if (subIsWord(str, l, (scasize(str) - 2) ) ) {
        return -1;// - infinity
    }

    i  = 0;
    ch = str[0];
    while (!scblank(ch)) {
        i = i+1;
        ch = str[i];
    }
    // i here is the first blank after l
    j = i+1;
    ch = str[j];
    while (scblank(ch)) {
        j = j+1;
        ch = str[j];
    }
    // j here is the first non-blank after i
    sep = j - i; 
    maxSubSep = maxSeparation(str, j);
    if (maxSubSep < sep ){
        max = sep ;
    } else { 
        max = maxSubSep;
    }
    return max;

    @post maxSpSpec {
        isMaxSeparation (str, 0, rv);
    }
    @behavior maxSpSpec {
        good {input={str="aaN",l=0};
              output={rv=-1}};
        bad {input={str="aaN",l=0};
              output={rv=0}};
        good {input={str="aa aa  aaa aaN",l=0};
              output={rv=2}};
        bad {input={str="aa aa  aaa aaN",l=0};
              output={rv=1}};
        bad {input={str="aa aa  aaa  aaN",l=0};
              output={rv=4}};
    }
}

boolean sameWords(int [] p1, int [] p2, int l1, int l2) {
    @pre swSpec { 
        subIsPara(p1, l1, (scasize(p1) - 1)); //p1[l1 .. |p1|-1] is a paragraph
        subIsPara(p2, l2, (scasize(p2) - 1)); // same for p2 with l2
    }
    return ( scaequal(p1,p2) && 
             subIsWord(p1,0,(scasize(p1)-2)) && 
             scnewline((p1[(scasize(p1)-1)]))) 
        ||
           ( exists (int w1:[l1 .. scasize(p1)-1], int w2:[l2 .. scasize(p2)-1]){
             (exists (int k1:[w1+1 .. scasize(p1)-1], int k2:[w2+1 .. scasize(p2)-1]) {
               scasubeq(p1,l1,w1,p2,l2,w2) && 
               headTailOfSub(p1,l1,w1,k1) &&
               headTailOfSub(p2,l2,w2,k2) &&
               sameWords(p1,p2,(k1+1),(k2+1))
             })
             });
    @post swSpec {
        subIsPara(p1, l1, (scasize(p1) - 1));
        subIsPara(p2, l2, (scasize(p2) - 1));
        ( scaequal(p1,p2) &&                   // p1 = p2 =word-newline
          subIsWord(p1,0,(scasize(p1)-2)) && 
          scnewline((p1[(scasize(p1)-1)]))) 
      ||
        ( exists (int w1:[l1 .. scasize(p1)-1], // p1=word-q1, p2=word-q2, sameWords(q1,q2)
                  int w2:[l2 .. scasize(p2)-1]){
             (exists (int k1:[w1+1 .. scasize(p1)-1], int k2:[w2+1 .. scasize(p2)-1]) {
               scasubeq(p1,l1,w1,p2,l2,w2) && 
               headTailOfSub(p1,l1,w1,k1) &&
               headTailOfSub(p2,l2,w2,k2) &&
               sameWords(p1,p2,(k1+1),(k2+1))
             })
             });
    }
    @behavior swSpec {
        good {input={p1="aaN",p2="aaN",l1=0,l2=0};
              output={rv=true}};
        good {input={p1="aa aaaNaaa  aaN",p2="aa  aaaNaaa aaN",l1=0,l2=0};
              output={rv=true}};
        good {input={p1="aaa  aa aaaNaaa  aaN",p2="aaa aa  aaaNaaa aaN",l1=5,l2=4};
              output={rv=true}};
        good {input={p1="aaa  aa aaaNaaa  aaN",p2="aaa aa  aaaNaaa aaN",l1=5,l2=4};
              output={rv=true}};
        good {input={p1="aaa  aaaa aaaNaaa  aaN",p2="aaa aa  aaaNaaa aaN",l1=5,l2=4};
              output={rv=false}};
        bad  {input={p1="aN",p2="aaN",l1=0,l2=0};
              output={rv=true}};
        bad  {input={p1="a aaNaaN",p2="a  aaNaaaN",l1=0,l2=0};
              output={rv=true}};
    }
}

boolean isJustified (int [] str, int l ){
    @pre isJustSpec {
        subIsPara(str, l, (scasize(str) -1));
    }
    return (subIsLine(str, l, (scasize(str) -1)) && 
            isMinSeparation(str, l, 1) &&
            isMaxSeparation(str, l, 1) &&
            (scasize(str) - l) <= W )
        ||
           (exists (int k:[l+1 .. (scasize(str) - 1)]) {
            subIsLine(str,l,k) &&
            subIsPara(str, (k+1), (scasize(str) -1)) &&
            isJustified(str,(k+1)) && 
            (k - l + 1 == W) &&
            (exists (int min:[0 .. (W/2)], int max:[0 .. (W/2)]) {
             isMinSeparation (str, l, min) &&
             isMaxSeparation (str, l, max) &&
             (max - min <= 1)
             })
             });
}

boolean isNWords(int [] str, int l, int r, int N) {
    @pre inNWordsSpec {
        subIsLine(str, l, r);
    }
    return 
        (subIsWord(str, l, r) && 
        scnewline((str[r])) &&
        N == 1)
    ||
        (exists (int k:[l .. r ]) {
         exists (int m:[k+1 .. r]) {
         headTailOfSub(str, l, k, m) && isNWords(str, (m+1), r, (N-1))
         } });
    @behavior inNWordsSpec{
        good {input={str="aaN", l=0,r=2,N=1};  
            output={rv=true}};
        good {input={str="aa aa aaN", l=0,r=8,N=3};  
            output={rv=true}};
        good {input={str="aa  aa  aaN", l=0,r=10,N=3}; 
            output={rv=true}};
        bad {input={str="aa  aa  aaN", l=0,r=10,N=2}; 
            output={rv=true}};
    }
}

boolean isNBlanks(int [] str, int l, int r, int N) {
    @pre inNBlanksSpec {
        subIsLine(str, l, r);
    }
    return 
        (subIsWord(str, l, r) && 
        scnewline( (str[r])) &&
        N == 0)
    ||
        (exists (int k:[l .. r ]) {
         exists (int m:[k+1 .. r]) {
         headTailOfSub(str, l, k, m) && isNBlanks(str, (m+1), r, (N-(m-k)))
         } });
    @behavior inNBlanksSpec {
        good {input={str="aaN", l=0,r=2,N=0};  // excess issue
            output={rv=true}};
        good {input={str="aa aa aaN", l=0,r=8,N=2};  // excess issue
            output={rv=true}};
        good {input={str="aa  aa  aaN", l=0,r=10,N=4};  // excess issue
            output={rv=true}};
        bad {input={str="aa  aa  aaN", l=0,r=10,N=2};  // excess issue
            output={rv=true}};
    }

}


boolean excessLessHeadOfNextLine(int [] str, int l, int r) {
    @pre excessSpec {
        subIsPara(str, l, r);
    }
    return subIsLine(str, l, r)
        ||
        (exists (int k:[l .. r], int m:[l .. r]) {
         subIsLine(str, l, k) && subIsLine(str, (k+1),m) &&
         excessLessHeadOfNextLine(str, (k+1), r) &&
         exists (int numW:[1 .. W], int numB:[1 .. W]) {
           isNWords(str, l, k, numW) && isNBlanks(str, l, k, numB) &&
           exists (int n1:[k+1 .. m], int n2:[k+1 .. m]) {
             headTailOfSub(str, (k+1), n1, n2) &&
             ((numB - numW) < (n1 - k))
           }
         }
         }
        );
    @behavior excessSpec {
        good {input={str="aaN", W=10};  // excess issue
            output={rv=true}};
        good {input={str="aa   aaa  aaaNaa aaaN", W=10};
            output={rv=false}};
        bad {input={str="aa   aaa  aaaNaa aaaN", W=10};
            output={rv=true}};
    }
}

boolean justify(int [] str) {
    int [] out;
    @pre jspec { scaempty(str) || para(str);}
    return true;
    @post jspec {
        (scaempty(str) && scaempty(out))
            ||
        ( (!scaempty(str))    && 
          para(out) && 
          sameWords(str, out, 0, 0) && 
          isJustified(out, 0) && 
          excessLessHeadOfNextLine(out, 0, (scasize(out) - 1)));
    }
    @behavior  jspec {
        good {input={str="", W=10}; output={out=""}};
        good {input={str="aaNaaa aaa aaa aaa aaaNaa aa aa aa aa aa aaN", W=10}; 
            output={out="aa aaa aaaNaaa    aaaNaaa  aa aaNaa  aa  aaNaa aaN"}};
        bad  {input={str="aaNaaa aaa aaa aaa aaaNaa aa aa aa aa aa aaN", W=10};  // not the same words
            output={out="aa aaa aaaNaa     aaaNaaa  aa aaNaa  aa  aaNaa aaN"}};
        bad  {input={str="aaNaaa aaa aaa aaa aaaNaa aa aa aa aa aa aaN", W=10};  // is not justified
            output={out="aa aaa aaaNaaa aaaNaaa  aa aaNaa  aa  aaNaa aaN"}};
        bad {input={str="aaNaaa aaa aaa aaa aaaNaa aa aa aa aa aa aaN", W=10};  // excess issue
            output={out="aa aaa aaaNaaa    aaaNaaa  aa aaNaa   aa aaNaa aaN"}};
    }
}