Helping programmers to adopt set-based specifications

Set theory is a key component of formal notations such as B, Z and Alloy. Set-based specifications are short while precise enough as to start the implementation. However, according to our experience, practitioners without a mathematical background find difficulties in using them. In this paper we propose the set-based programming language {log} as an aid to teach programmers to write set-based specifications. In one hand, a large class of set-based specifications can be automatically translated into \setlog programs, which can be used as prototypes; on the other hand, plain \setlog programs can be used as contracts, which are closer to the implementation. This could help in a widest adoption of set-based specifications since programmers seem to be adopting contracts as a form of specification.