======
>>> main.whiley
// Test extracted from Minesweeper
type uint is (int x) where x >= 0
type Board is {
bool[] squares, // Array of squares making up the board
uint width, // Width of the game board (in squares)
uint height // Height of the game board (in squares)
} where width*height == |squares|
/**
* Return maximum of two integer variables
*/
property max(int a, int b) -> (int r):
//
if a < b:
return b
else:
return a
/**
* Return minimum of two integer variables
*/
property min(int a, int b) -> (int r):
//
if a > b:
return b
else:
return a
function determineRank(Board b, uint col, uint row) -> uint
requires col < b.width && row < b.height:
uint rank = 0
// Calculate the rank
for r in max(0,row-1) .. min(b.height,row+2):
for c in max(0,col-1) .. min(b.width,col+2):
bool sq = get_square(b,(uint) c, (uint) r)
if sq:
rank = rank + 1
//
return rank
// Return the square on a given board at a given position
export function get_square(Board b, uint col, uint row) -> bool
// Ensure arguments within bounds
requires col < b.width && row < b.height:
int rowOffset = b.width * row // calculate start of row
assume rowOffset >= 0
assume rowOffset <= |b.squares|-b.width
return b.squares[rowOffset + col]
public export method test():
Board b = {width:3, height: 3, squares: [
false,false,true,
false,false,false,
true,false,true]}
assume determineRank(b,0,0) == 0
assume determineRank(b,0,1) == 1
assume determineRank(b,0,2) == 1
//
assume determineRank(b,1,0) == 1
assume determineRank(b,1,1) == 3
assume determineRank(b,1,2) == 2
//
assume determineRank(b,2,0) == 1
assume determineRank(b,2,1) == 2
assume determineRank(b,2,2) == 1
---