Helping Programmers to Adopt Set-Based Specifications

CRISTIÁ, MAXIMILIANO; ROSSI, GIANFRANCO; FRYDMAN, CLAUDIA

Workshop; Proceedings of the First Workshop on Formal Methods in Software Engineering Education and Training, FMSEE&T 2015; 2015

Set theory is a key component of formal notations such asB, Z and Alloy. Set-based specifications are short while precise enoughas to start the implementation. However, according to our experience,practitioners without a mathematical background find difficulties in us-ing 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 automati-cally translated into {log} programs, which can be used as prototypes;on the other hand, plain {log} programs can be used as contracts, whichare closer to the implementation. This could help in a widest adoption ofset-based specifications since programmers seem to be adopting contractsas a form of specification.