In the example code given in VccDemo: Bakery.c, and another file Rundown.c given in examples in testsuite. It would be great if one could tell, what does these programs do. It would help better understand the specifications and how did we come up to invariants and spec variables used.

Thanks.