Logic for HackersSpring 2014Computer Science DepartmentBrown University |
MWF 10-11
CIT 368
Software Abstractions by Daniel Jackson
Electronic copy from Brown Library
We will use Alloy.
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.)You may not discuss your work with anyone other than course staff, except a partner on a group assignment. You are responsible for keeping your files secure, etc.
Logic plays a central role in describing systems. In addition, logic offers the foundation for a rich set of tools for reasoning about systems, namely, determining whether they have been described correctly relative to our expectations.
Unfortunately, this fascinating set of activities can come across to some as rather drab and pedantic. In turn, logic often fails to take hold of computer science imaginations because it seems to be a collection of statements about the state of Socrates and rain, not about the state of buffers and caches and the other difficulties that everyday practicing computer scientists wrestle with.
This course attempts to address this problem by re-focusing logic on computer systems. We will use logic to describe systems and then analyze our descriptions of them. We will use modern tools that ease the description and automate the analysis. In the process we will try to re-imagine the way we think about not only describing but even designing complex modern computer systems.