spec module View // calls Board
{
    format Cell;
    format WindowConfig;
    format BoxConfig;

    proc clickStatus(x:int; y:int) returns r:int ensures true;
    proc drawBox(bcf:BoxConfig) ensures true;
    proc drawBoxOutline (bcf:BoxConfig; col:int) ensures true;
    proc drawRect (x0:int; y0:int; w:int; h:int) ensures true;
    proc drawStringInBox (str:string; bcf:BoxConfig; col: int) ensures true;
    proc eraseBox(bcf:BoxConfig) ensures true;
    proc makeBox(x:int; y:int; w:int; h:int; bw:int; r:int) 
      returns b : BoxConfig ensures true;
    proc drawCell(c:Cell)
      requires (c in Board.U) & (card(c) = 1)
      calls Board ensures true; // has some transitive calls
    proc drawNumCC (ci:Cell) calls Board ensures true;
    proc drawMineCC (ci:Cell) ensures true;
    proc drawFlagCC (ci:Cell) ensures true;
    proc drawCrossCC (ci:Cell) ensures true;
    proc drawFlagSwitch(on:bool) ensures true;
    proc printScore(nbcto:int; nbfc:int) ensures true;

    proc makeWcf(nbcols:int; nbrows:int; nbmines:int) 
      returns w:WindowConfig ensures true;
    proc openWcf() ensures true;
    proc ending(s:string) 
      requires Board.init & Board.gameOver & (Board.UnexposedCells <= Board.U) 
      modifies Board.ExposedCells, Board.UnexposedCells 
      ensures card(Board.UnexposedCells') = 0;

    // click finding
    proc returnClickX(x:int; y:int) returns x1:int ensures true;
    proc returnClickY(x:int; y:int) returns y1:int ensures true;

    proc drawFieldInitial() calls Board ensures true;
    proc drawFlagTitle() ensures true;
    proc coor(x:int; y:int) returns c:Coord ensures true;
    proc drawClosedCC (ci:Cell) ensures true;

    proc getCellCoord(ci:Cell) returns c:Coord 
      suspends Board.NP calls Board ensures true;
    proc openCCell (ci:Cell) suspends Board.NP ensures true;
    proc closeCCell (ci:Cell) suspends Board.NP ensures true;

    proc drawFieldEnd() 
      requires Board.init & Board.gameOver & (Board.UnexposedCells <= Board.U)
      modifies Board.ExposedCells, Board.UnexposedCells calls Board 
      ensures card(Board.UnexposedCells') = 0;
    proc drawCellEnd(c:Cell)
      requires (c in Board.U) & (card(c) = 1) & Board.init 
      calls Board ensures true;
}