Lab 1 Formal Design with B, Master 1, 2011-2012 -------------------------------------------------------------------------------- 1. Customize your Atelier B settings by following the instructions given in the text file Atelier-B-Setup.txt. 2. Download the B components in the Examples subdirectory, and add them to a new Atelier B project. Familiarize yourself with the user interface of the tool: - Type-check the B components. - Generate proof obligations. - Call the automatic prover from the main window. - Inspect the proof obligations with the interactive prover. 3. Generate C code for the developed module Hello, and compile it. Recall that the necessary steps are given in Atelier-B-Setup.txt. 4. Using ProB, animate the Switch and Population abstract machines. Adjust ProB preferences to widen the range of animation settings.