Created
November 13, 2019 15:27
-
-
Save zelinskiy/a6802f6a93ef0065ea4413ecb568e545 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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; | |
} | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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); | |
} | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment