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.

Helping programmers to adopt set-based specifications / Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia. - ELETTRONICO. - 1385:January(2015), pp. 3-10. ((Intervento presentato al convegno 1st Workshop on Formal Methods in Software Engineering Education and Training, FMSEE and T 2015 - co-located with the 20th International Symposium on Formal Methods, FM 2015 tenutosi a Oslo (Norvegia) nel 2015.

Helping programmers to adopt set-based specifications

ROSSI, Gianfranco;
2015

Abstract

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.
Helping programmers to adopt set-based specifications / Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia. - ELETTRONICO. - 1385:January(2015), pp. 3-10. ((Intervento presentato al convegno 1st Workshop on Formal Methods in Software Engineering Education and Training, FMSEE and T 2015 - co-located with the 20th International Symposium on Formal Methods, FM 2015 tenutosi a Oslo (Norvegia) nel 2015.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11381/2801110
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact