Software

Alloy

Please download and install Alloy 4.2 on your machine. You'll need to install Java to run Alloy.

In the configuration, please change the setting for Forbid overflows from off (which is the default) to on. On OS X, go to the Options menu and select the last entry. Nothing will appear to happen, but when you look at the menu again, the setting will be on.

Z3

Note that we encourage the use of department machines for the Z3 assignment. Running 'source /course/cs195y/src/venv/bin/activate' in your Terminal will place you in the course's Python environment, which already has the Z3 library installed.

If you'd like to also install Z3 on your local machine:

1. Go to https://github.com/Z3Prover/bin/tree/master/releases
2. Choose the file z3-4.4.1-XXXX where XXXX is your operating system version
3. Click "View Raw". This will prompt the download window.
4. Extract the file to a directory, say, /path/to/z3
5. When running Python, instead of using python pythagorean.py, use PYTHONPATH=/path/to/z3/bin python pythagorean.py instead.

Spin

You can download Spin via the Spin Website. The software should also be pre-installed on lab computers.

Liquid Haskell

We suggest that you to use LiquidHaskell via this browser-based IDE