Set theory is a key component of formal notations such as B, Z and Alloy. Set-based speci cations are short while precise enough as to start the implementation. However, according to our experience, practitioners without a mathematical background nd di culties in using them. In this paper we propose the set-based programming language flogg as an aid to teach programmers to write set-based speci cations. In one hand, a large class of set-based speci cations can be automatically translated into flogg programs, which can be used as prototypes; on the other hand, plain flogg programs can be used as contracts, which are closer to the implementation. This could help in a widest adoption of set-based speci cations since programmers seem to be adopting contracts as a form of speci cation.
fa? 7! sa(a?) + m?g _ (a? 2= dom sa _ m? (Set) where variables decorated with ' ?' are meant to be input parameters; variables decorated with a prime are meant to be the value of a state variable in the next state; a? is the account where the amount m? is intended to be deposited; and the operator roughly updates a function [14, page 102]. Note that in this model, partial functions are sets of ordered pairs. For this reason we call it a set-based speci cation.
From now on, the term set will include binary relations, partial and total
functions, and bags (multisets). In e ect, all these structures can be expressed
in terms of set theory as shown for example in [
An alternative model, and perhaps closer to a possible implementation, is based on lists instead of partial functions. In this case we can de ne sa 2 seq(ID Z) and the speci cation for depositing money becomes1: 9 s1; s2 2 seq(ID
Z); b 2 Z : m? > 0 ^ sa = s1 a h(a?; b)i a s2 ^ sa0 = s1 a h(a?; b + m?)i a s2 _ ((a?; b) 2= sa _ m? where a is is the list concatenation operator. This speci cation is more complex because there is no easy way of expressing the modi cation of a list element without having its position.
As can be seen, the list-based speci cation is harder to understand than the set-based one. We think that the true problem is that the savings accounts of a bank are not a list but, essentially, a partial function. This is a recurring observation in software speci cation: many real-life entities are, essentially, sets, binary relations or partial functions (seen as sets). They are not lists, trees or hash tables. Therefore, set-based speci cations should be favored over other notations if the goal is to describe the essence of the problem to be implemented.
A third model could be based on design-by-contract (DBC) notations such as
the Java Modeling Language (JML) [
According to our experience, programmers feel more comfortable with
contracts such as (JML) than with speci cations such as (Set). The reasons may be
in the following facts: a) the contract language is closer to the implementation
language thus increasing the learning curve; b) the possibility of using data
structures present in the standard library of the programming language and program
variables as part of the contract; c) contracts can involve structural properties
such as inheritance, information hiding, etc.; d) contracts are given as program
annotations rather than as a separate description; and e) some of these DBC
notations include tool support for runtime checking, static veri cation and test
case generation [
However, the Software Engineering and Formal Methods communities for years have supported the notion that speci cations should be more abstract than their implementations. Clearly, each DBC notation is tightly coupled with a given programming language, thereby, necessarily oriented towards speci c implementation choices.
Hence, as Software Engineering instructors we are faced with two problems regarding set-based formal speci cations: a) speci cations should be abstract and set theory provides a sound foundation for this for many systems; and b) contracts are more appealing to programmers but not as abstract as speci cations and they seldom use set theory.
In order to tackle these problems from an educational perspective, in this paper we propose to use a combination of set-based speci cations, such as (Set), and flog g (pronounced `setlog') programs. flog g is a constraint logic programming (CLP) language implementing a very general theory of sets. As such it can determine satisfability for a wide range of set formulas. Therefore, flog g can be used both as a tool beneath a set-based speci cation language such as Z or B, and as the basis of a set-based contract language. In this way, it can be closer to an implementation, like DBC contracts, but it enables set-based speci cations, like speci cation languages.
We believe that flog g can help during the teaching process of software speci cation. It can give an operational, programming-oriented view of set theory to students while forcing them to write set-based speci cations. 2
The problems listed below were identi ed by the authors while teaching set theory, programming and formal speci cation in mandatory courses of several undergraduate degrees in Argentina, France and Italy for many years, and as occasional trainers for practitioners.
From now on student means a person enrolled as a student in a university degree as well as a practitioner taking a training course.
We have identi ed the following problems regarding the use of set theory as the basis for software formal speci cation. Students tend to think in terms of the data structures they have already learned and used. This means that it is hard for them to represent a particular concept in the requirements as a set. They hardly \see" a set in the requirements. For example, in the context of information systems, the rst data structure they think of is a table. Only after they learn that tables are either relations or partial functions, they start to feel comfortable with them.
Often they think that it is a waste of time to nd the best set-based structure for a concept if they are going to end up implementing it as a hash table, a tree or any other implementation-level data structure. They need to see how concise many properties become when they are expressed in terms of sets rather than in terms of implementation-oriented data structures.
This problem may be originated in two sources: the complexity of working at more than one level of abstraction; and the fact that students are used to work with certain kind of languages and data structures.
The lack of control structures is a source of problems rather than an aid. Students, but mostly experienced programmers, nd many troubles in formalizing a requirement without control structures. A declarative language seems to be incomplete for them. Even speci cations that take the form of state machines pose problems. A typical case is representing a loop as a state transition that is enabled until some precondition becomes false (and thus the transition is disabled) and at that moment another state transition becomes enabled. Another typical case is to make them understand that many times it is not even necessary at all to specify a loop because a (declarative) set formula does the job. Sometimes they have doubts about the result of a particular set formula. This is a problem that surfaces during the initial classes due to the many set and relational operators they need to learn. Some times you can see them guring out if a given formula yields the desired result by computing some examples. Frequently they use universal quanti cations when a quanti cation-free formula would work.
They experience problems in reconciling the speci cation with the implementation. Set-based notations are meant to produce a speci cation document separated from the implementation. From a Software Engineering perspective we completely agree with this approach. However, from an educational perspective we observe that students do not clearly see the role and implications of the speci cation document in the development process. Perhaps the major di culty is to comprehend the relation between the speci cation and the design document (i.e. the document describing the software components, their functionality and the relationships between them [7, chapter 4]). For instance, they ask questions such as \is a state transition the speci cation of a method?", \where the state invariant must be implemented?", \should the caller be responsible for checking the precondition or should be the callee?".
We think that a combination of flog g, DBC and set-based speci cations can help students in solving many of these problems making it easier for them to adopt the latter. 3
flog g as an Aid for Set-Based Speci cations
flog g is a CLP language based on Prolog where sets are rst-class entities [
For example, (Set) can be translated into the following flog g code: dom(Sa; D ) & (A in D & M > 0 & apply(Sa; A; B ) & oplus(Sa; f[A; B ]g; NSa)) or ((A nin D or M =< 0) & NSa = Sa) which is operationally interpreted as a sequence of calls to prede ned procedures that implement the basic operations on sets, partial functions and integers. If the flog g interpreter executes this code it will end up in one of three ways (much as SAT or SMT solvers would do): returning a solution to the goal, answering \no", or getting a timeout.
For example, if oplus(Sa; f[A; B ]g; NSa) is executed the rst answer of the interpreter is2 NSa = {[A,B]\Sa}, where {[A,B]\Sa} means f[A; B ]g [ Sa.
We have shown that a very general fragment of set-based speci cations can
be automatically translated into flog g [
Although flog g is a declarative programming language, students may feel
more comfortable with it than with plain set-based speci cations since many of
them are experienced programmers. Thus flog g can help in reducing the gap
between speci cations and programs. Moreover, it could be used to describe
contracts. For instance, (JML) can be expressed in flog g terms as follows:
public normal behavior
public exceptional behavior
requires dom(Sa; D ) & A in D & M > 0
ensures apply(Sa; A; B ) & oplus(Sa; f[A; B ]g; NSa)
requires dom(Sa; D ) & A nin D or M =< 0
ensures NSa = Sa
(flog g-JML)
where a simple naming convention between contract (or speci cation or flog g)
variables and program variables can be established. Given that the flog g
predicates present in the requires and ensures clauses are executable programs, this
2 We have simpli ed the output generated by the interpreter for presentation issues.
contract could in principle be used for runtime checking as the JML contract,
and it can also be used for test case generation [
Although (JML) and (flog g-JML) may give the impression that contracts written in JML and flog g have a similar complexity, it is not true in general. flog g contracts will tend to be simpler because they can take advantage of a larger set of operators like domain restriction, relational image, and so forth. These operators are not implemented in the Java classes delivered with the standard library.
In a sense, (flog g-JML) is at an intermediate abstraction level between (JML) and (Set), enjoying some of the properties of both ends. Since students feel comfortable with programming languages, then taking them from an imperative programming language to contracts written in terms of sets to set-based speci cations may help them in overcoming all the di culties they nd when they are directly introduced into the world of formal speci cation. 4
Teaching Proposal for Set-Based Software Speci cation In this section we set forth a teaching proposal to introduce students into the world of set-based speci cations. The proposal is based upon the idea of gradually taking students from DBC to formal notations such as Z and B. This proposal uses flog g as the linking tool between the world of DBC and that of set-based speci cations.
Our proposal assumes that students: { Are aware of a programming language such as Java; { Understand the de nition of program correctness. Speci cally, they are conscious of: a) the existence of two distinct documents: the speci cation (S ) and the implementation (P ); and b) that S is authoritative over P ; and { If they have not had previous exposure to DBC, they will nd it natural and intuitive as an extension of their programming skills.
Based on these assumptions, we propose the following teaching process: 1. Teach DBC.
Pick the notation that best suits the programming skills of your audience. If your goal is to introduce students to set-based formal notations do not go deep into DBC. Recall that the nal idea is that students use set-based speci cations as contracts. 2. Teach set theory by means of flog g.
We suggest to follow the work plan set forth by Abrial in Z and B [
This is perhaps the most di cult step because it implies to force students to think in set terms rather than in implementation-level data structures. The best course of action we have found is to show to them that many implementation-level data structures either: a) obscure the essential properties of the data being represented because they were thought as e cient representations (but e ciency need not to be part of a speci cation); or b) usually the operations de ned on their interfaces complicate the formalization of simple properties. 4. Teach a speci cation language such as Z or B and its relationship to flog g and DBC.
Most text books on formal speci cation present speci cations as documents with no relation with the software design. In general, a speci cation is presented as a formalization of the functional requirements, which must not talk about design features|such as information hiding, connectors, inheritance, etc. We agree with this view, although we think that it may be too alien for students used to program non trivial software. These students tend to think in terms of components with interfaces which implement some functionality. Therefore, we consider that the rst students' approach to formal speci cation should be as a complement to a software design. More concretely, formal speci cation should be introduced as a technique to clearly and concisely document the functionality of design components. Particularly, the fraction of a set-based formal notation that can be automatically translated into flog g should be used as the DBC notation.
The full set-based notation can be used if you do not plan to introduce some
form of automatic veri cation, because it would need to link some tools.
If the fraction mentioned above is used, our approach allows to automatically
build prototypes from a combination of Z and user interface speci cations
[
As advocates of formal methods we permanently look for ways to make industry to adopt them more widely. One of the reasons we frequently see that impedes a wider use of formal methods is the relatively poor mathematical background of practitioners. This goes against techniques which require the explicit use of some form of formal methods.
In this paper we intend to provide teachers with a more gentle way to introduce students to the world of formal notations like B and Z. We propose to go from DBC, to set theory, to flog g and nally to a set-based notation. Consider that in order to fully use this teaching process some tools need to be developed.
However, our proposal might be just a patch. Maybe we should ask ourself whether programming must be taught before speci cation as we currently do| after all, our community has been advocating for years that, in development projects, speci cation must precede implementation. Have we been mistaken all these years? Or are we teaching the other way around? To formalize or not to formalize that is... not the question: you are going to write code anyhow. The real question is: how many times are you going to formalize?