For this problem set, you are to turn in an overview document covering Part 2.
The overview document should be composed as described in
You may work on this problem set with a partner. We strongly recommend discussing, critiquing, and agreeing on specifications before doing any implementation. You can also bring specs to office hours to get feedback. When critiquing a spec, think about the spec both from the standpoint of the client who is going to use the spec, and the developer who must implement it. It is also a good idea to discuss and agree on abstraction functions and rep invariants for your data structures. You will also need to think about how to divide your program into modules.
We will be holding 20-minute design review meetings during October 19–22. Your group is expected to meet with one of the TAs or the instructor during their office hours, or with consultants during consulting hours. A signup schedule is available on CMS. You should be able to explain your design in about 10 minutes, leaving 10 minutes for questions. It's a good idea to practice your presentation ahead of time so you use your time effectively.
In your design review, plan to talk about at least:
Prove the following statements using only the inference rules provided in Lecture 12: Natural Deduction (don't use any of the tautologies).
Prove the following statements using the inference rules for propositional logic in Lecture 11: Natural Deduction and the rules for quantifiers in Lecture 12. Note that p, q are names of predicates.
Suppose we have a function
max with the following spec:
(* Requires: ⊤ * Returns: r = max(x,y) where (r=x∨r=y) ∧ r≥x ∧ r≥y *)
Now we implement a function that takes the maximum of three numbers as follows:
(* Requires: ⊤ * Returns: max3(x,y,z) = r * where (r=x ∨ r=y ∨ r=z) ∧ r≥x ∧ r≥y ∧ r≥z *) let max3(x,y,z) = if x <= y then max(y,z) else max(x,z)
max3satisfies its spec.
The second part of this problem set involves implementing Conway's Game of Life in OCaml.
It might help to play around with the system in any one of many available implementations online to obtain a better grasp of the consequences of these rules.
All state transitions occur across the entire board at the same time.
That is, if we consider the current state of the game to be represented
as the state of each cell on the board, then the next state of the game
is one in which the above transition function is applied once to each
cell simultaneously. We call this board transition a tick. One can
imagine a slight variation on this game in which live cells also contain
an RGB color represented as a 3-tuple of integers, each between 0 and
255. To support color, the transition rules given above are
When a live
cell is kept alive by its 2 or 3 neighbors, its color remains unchanged.
However, when a dead cell is brought to life by its three
neighbors, its color is computed from the average color of those
evolve_color function computes the new
color of the cell, given the average color of the neighbors.
Your main task is to implement a
GameOfLife module incorporating
the rules above. As discussed in greater detail below, we've given
you a functional interface to OCaml's graphics libraries that allows
you to display and modify the state of your game in a GUI. The way you use
your functions to update the GUI is intrinsically tied to your design, and you
should consider this carefully when defining the state for GameOfLife. The
GAMEOFLIFE interface is left up to you, but we do expect you to
Your implementation should incorporate a few key clarifications. The game's universe is square, with a power-of-2 number of cells in each dimension. Cells occur at integer coordinates in this space. The lower left cell is (0,0) and the upper right is (2n - 1, 2^n - 1) for board size n. However, the GUI is always centered between cells. Thus, if the window was centered on cell (x,y), the view would be centered on cell (x+0.5, y+0.5).
The viewing window is always centered between cells, so we
cannot zoom indefinitely. Because the viewing window is limited to
512 × 512 pixels, it does not make sense to zoom
in further than
When the level of zoom is such that each viewing window pixel represents
several cells in the game of life, the color of the cell in the GUI should be
based on the average color of all cells that fall within
that window pixel, including dead cells, which are black (0,0,0).
The game board may be very large, so your representation should allow for efficient zooming at powers of two as described above and accommodate very large boards as long as they are sparsely populated; your implementation should handle sparse populations on board sizes as large as 224×224 efficiently. To assure this, run time must not grow linearly with the size of the board. Be sure that you have a good understanding of what is required for all parts of the assignment before you design the state representation.
We are providing a module
Graph, which provides functionality
for computer graphics and graphical user interfaces.
It has the following signature:
This module requires the use of two libraries that are not automatically loaded into OCaml: graphics.cma, and unix.cma. To load these libraries into the top level environment, run the following commands before compiling the code:
#load "graphics.cma";; #load "unix.cma";;
We are distributing a top-level OCaml environment that has these libraries
ocamlg. You're code must compile on this
environment without any
#load commands. If you are using Emacs,
you can use this top-level environment while developing; when it asks which
top-level environment to load, point Emacs to the directory containing
ocamlg. For ease, you may dump ocamlg into the default directory.
On Windows, this is:
C:\Program Files\Objective Caml\bin.
Note that this environment is a Windows binary. If you are running a linux/mac, you can create your own top level environment with the following command:
ocamlmktop -o ocamlg "graphics.cma" "unix.cma"
You are required to implement a module GUI. It should have the following two functions implemented, as well as any other function you see fit:
(* loadPattern s loads the game defined in file s *) loadPattern: string -> unit (* startNew creates a new, empty game of life *) startNew: unit -> unit
Both of these functions should open a 512 by 512 pixel window, and the game
should start running (as opposed to being paused). You are required to
implement a function
loadPattern, allowing games to be loaded
based on a state description in a file.
A correctly formatted file has a first line that gives the size n of the board. After that, it contains a series of lines describing rows of the state of the game near the origin (0,0). Each line contains a sequence of the characters ".", "r", "g", or "b". The character "." means that there is a dead cell. The characters "r", "g", and "b" represent cells that are initially alive, with colors red (255, 0, 0), green (0, 255, 0), or blue (0,0,255). The program should check that all lines have the same length. The described cells are loaded so that the loaded pattern is centered on the position (2n-1,2n-1) as nearly as possible. For example, here is the format for a red vertical blinker in a 23×23 board:
3 .r. .r. .r.
Loading this should create an 8x8 board, with red cells alive at positions (4,3), (4,4), and (4,5). On the next step, it will change to a horizontal blinker.
Besides updating the game board in accordance with the rules of the game of life, you are also required to provide the following functionality in your program:
The following features can be implemented for good karma:
Unix.gettimeofday(), which gives the current time, may be useful for this.
Please submit the following files:
Submit a file called
answers to the questions in part 1.
Submit all the files you worked on for your
Game of Life implementation. Please note: you do not have to submit
we will be using the implementations we provided. You should submit a
file for this part called
part2.zip, which contains:
gameOfLife.mli. The latter file contains your specification for the game of life. The latter file contains your implementation.
gui.ml. This file should contain a module called GUI, as described above.
others.txtthat lists the files you have submitted and explained their purpose.