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.