OpenJML Examples: Change Case

This example simply changes the case of an ASCII letter. It was mostly used as a basis for seed bugs and to demonstrate tracing and debugging techniques.

public class ChangeCase {

  //@   requires 'A' <= c <= 'Z';
  //@   ensures 'a' <= \result <= 'z';
  //@ also
  //@   requires 'a' <= c <= 'z';
  //@   ensures 'A' <= \result <= 'Z';
  //@ also
  //@   requires !('A' <= c <= 'Z') && !('a' <= c <= 'z');
  //@   ensures \result == c;
  public char changeCase(char c) {
    char result = ' ';    
    if (c > 'z') {
      result = c;
    } else if (c >= 'a') {
      result =  (char)(c - 'a' + 'A');
    } else if (c > 'Z') {
      result =  c;
    } else if (c >= 'A') {
      result =  (char)(c - 'A' + 'a');
    } else {
      result = c;
    }
    return result;
  }

}