1.
a) Kyllä, loppuehdoissa on näin määritelty
b) Kyllä, loppuehdossa ei ole määritelty muutakuin että palautettavassa taulukossa arvot ovat
suuruusjärjestyksessä. Arvoilla ei siis ole välttämättä mitään tekemistä t taulukon kanssa.
c) Ei, loppuehdon määrittelyn mukaan palautettavan taulukon alkioden arvot voivat olla samat.
d) Kyllä, ainoastaan tämä on mahdollista ilman että loppuehtoa rikottaisiin.
2.
a)
/**
* @. pre rek != null
* @. post a = rek.indexOf('-');
* RESULT = false if(rek.length() < 4 || rek.length() > 7)
* RESULT = true if (a != null &&
* FORALL(i: 0 <= i < a; Character.isLetter(rek.charAt(i)) == true)
* && FORALL(i: a < i < 7; Character.isDigit(rek.charAt(i)) == true )
*/
public static boolean onkoRekisterinumero(String rek)
b)
/**
* @.pre taul != null && merk != null
* @.post RESULT == FORALL(i: i < taul.length; taul[i].indexOf(merk) != -1)
*/
public static boolean sisältääköMerkin(String[] taul, char merk)
3.
a)
/**
* @.pre prefix != null
* @.post RESULT == (prefix.length() <= this.length() & ( prefix == null || this.equals(prefix) ||
* FORALL(i: 0 <= i < prefix.length(); this.charAt(i) == prefix.charAt(i)) ) )
*/
boolean startsWith(String prefix)
b)
/**
* @.pre oldChar != null && newChar != null
* @.post RESULT = uusi stringi, jossa kaikki this stringin oldchar merkit on korvattu newChar merkillä ||
* RESULT = this if(this.indexOf(oldChar) != -1)
*/
String replace(char oldChar, char newChar)