Preliminaries

This class will build on the basics of discrete math.

Mathematics for Computer Science by Eric Lehman, F Thomson Leighton, and Albert R Meyer is a good free, online textbook for this (though it goes into much more detail than we'll need in CS340).

Specific helpful chapters include:

- Ch. 3: Logical Formulas:
    - 3.1 Propositions from Propositions (and, or, not, implies) 
    - 3.2 Propositional Logic in Computer Programs 
    - 3.3 Equivalence and Validity (contrapositive, satisfiability)
    - 3.5 The SAT Problem
- Ch. 4: Mathematical Data Types 
    - 4.1 Sets 
    - 4.3 Functions
    - 4.4 Binary Relations

Discrete Structures lecture notes by Vladlen Koltun also provide a good overview.

Creating executables (for PBT)

Here are some notes on creating executables for the PBT assignment (and beyond).

Alloy

Textbook (note: a copy will be available in Workshop each week that you can access, we recommend getting your own copy if feasible): Software Abstractions: Logic, Language, and Analysis, Revised Edition by Daniel Jackson.

Note: the textbook is based on a earlier version of Alloy (Alloy 4.0) that does not include temporal logic keywords (e.g., always, eventually, before, after).

Alloy 6 has its own documentation and (work in progress) online textbook, by Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo.

AlloyDocs is a work in progress additional reference documentation for Alloy, including Alloy 6, by Hillel Wayne.