As a start, we give further examples of Alloy specifications. Next we turn to specification of imperative programs. Assertions about programs are specifications of how the program is supposed to behave. Assertions can be used for correctness reasoning and for testing. We illustrate the important notions of preconditions and postconditions. We demonstrate how the state transitions of imperative programming can be modelled as relations in Alloy. Correctness reasoning can be linked to testing and debugging by means of executable assertions, and by means of random generation of test cases based on preconditions and postconditions.