@Inproceedings{EPTCS79.2, author = {Back, Ralph-Johan and Eriksson, Johannes}, year = {2012}, title = {An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support}, editor = {Quaresma, Pedro and Back, Ralph-Johan}, booktitle = {{\rm Proceedings First Workshop on} CTP Components for Educational Software, {\rm Wroc{\l}aw, Poland, 31th July 2011}}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {79}, publisher = {Open Publishing Association}, pages = {29-48}, doi = {10.4204/EPTCS.79.2}, }