Person.java

package org.jmlspecs.samples.jmltutorial;

public class Person {
  private /*@ spec_public non_null @*/ String name;
  private /*@ spec_public @*/ int weight;

   /*@ public invariant !name.equals("")
    @         && weight >= 0; @*/

  /*@ also
    @ ensures \result != null
    @   && (* \result is a displayable
    @       form of this person *);
    @*/
  public String toString() {
    return "Person(\"" + name + "\","
      + Integer.toString(weight) + ")";
  }


  //@ ensures \result == weight;
  public /*@ pure @*/ int getWeight() {
    return weight;
  }


  /*@requires kgs >= 0;
    @requires weight + kgs >= 0;
    @ensures weight == \old(weight + kgs);
    @*/
  public void addKgs(int kgs) {
    if (kgs >= 0) {
      weight += kgs;
    } else {
      throw new IllegalArgumentException();
    }
  }


  /*@ requires n != null && !n.equals("");
    @ ensures n.equals(name)
    @   && weight == 0; @*/
  public Person(String n) {
    name = n; weight = 0;
  }
}

SlidingTilePuzzle.java

import java.util.Random;

public class SlidingTilePuzzle {
    private /*@ spec_public non_null @*/ int[] tiles = {
         1,  2,  3,  4,
         5,  6,  7,  8,
         9, 10, 11, 12,
        13, 14, 15,  0
    };
    private /*@ spec_public @*/ final int size = 4;
    private /*@ spec_public @*/ int hole = 15;

    /*@ public invariant tiles[hole] == 0
    @         && tiles.length == size * size; @*/

    public SlidingTilePuzzle() {}

    public void shuffle(int moves) {
        Random rand = new Random();
        int[] neighborOffsets = { -size, +size, -1, +1 };
        while (moves --> 0) {
            int neighbor;
            do {
                neighbor = this.hole + neighborOffsets[rand.nextInt(4)];
            } while (!this.canMove(neighbor));
            this.move(neighbor);
        }
    }

    public /*@ pure @*/ boolean canMove(int pos) {
        if (pos < 0 || pos >= size * size) {
            return false;
        }
        int diff = this.hole - pos;
        if (diff == -1) {
            return pos % size != 0;
        } else if (diff == +1) {
            return this.hole % size != 0;
        } else {
            return Math.abs(diff) == size;
        }
    }

    //@ ensures tiles[pos] == 0 && canMove(pos);
    public void move(int pos) {
        if (!this.canMove(pos)) {
            throw new IllegalArgumentException("Illegal move");
        }
        this.tiles[this.hole] = this.tiles[pos];
        this.tiles[this.hole = pos] = 0;
    }
    
    //@ ensures pos >= 0 && pos < tiles.length;
    //@ ensures \result == tiles[pos];
    public int tileAt(int pos) {
        return this.tiles[pos];
    }

    //@ ensures \result == hole;
    public /*@ pure @*/ int getHole() {
        return this.hole;
    }
    
    /*@ also
    @ ensures \result != null
    @   && (* \result is a displayable
    @       form of this game state *);
    @*/
    public String toString() {
        StringBuilder sb = new StringBuilder(size * size * 4);
        for (int i = 0; i < size; i++) {
            for (int j = 0; j < size; j++) {
                int tile = this.tileAt(i * this.size + j);
                sb.append(String.format("%2s ", (tile == 0) ? "" : Integer.toString(tile)));
            }
            sb.append("\n");
        }
        return sb.toString();
    }

    // Demonstration
    public static void main(String[] args) {
        SlidingTilePuzzle p = new SlidingTilePuzzle();
        for (int i = 0; i < 20; i++) {
            System.out.println(p);
            p.shuffle(1);
        }
    }
}