”La main `a la pâte”, An Abacus to Teach Formal Specifications

http://www.bcs.org/upload/pdf/ewic_tfm06_paper8.pdf

La main à la pâte, un boulier pour enseigner les spécifications formelles

This paper describes the use of a soroban (japanese abacus) for teaching abstraction
and refinement in a introductory course on B specifications.
Teaching Formal Methods: Practice and Experience, 15 December 2006
The British Computer Society
Keywords: B method, abacus, numeral systems, abstraction, refinement