The main motivation of SLAM is to give an answer to the question ``why formal methods are not more extended?''. One reason is that formal methods are perceived as an improductive process, from our point of view, mainly because after the system has been formaly specified it is still necessary to hand-code the program, and because there is no tools that support formal methods through the entire development process.
Our thesis is that a formal specification contains such a quantity of useful information that productivity problems would dissapear. But the problem now is that there is no good tool support to write specifications nor to extract and effectively use that information. The problem of incorporating rigourous methodologies in the development process could be mitigated with the same solution: tools supporting formal methods through the whole development process.
SLAM is a software tool which seeks to facilitate the production of correct software. Introduction of formal methods in the development process, specifically in design and programming stages, is one of our objectives.
The system is composed by two elements: a programming environment which integrates tools like verifiers or code synthesizers, and, Slam-sl, a formal specification language.
The Slam development environment is responsible for allowing the user to declare the full specification in a convenient and friendly way. In order to facilitate the understanding of Slam-sl we will show its elements with a text syntax that does not necessarily correspond neither with an internal representation nor the system presentation, so the reader should not pay too much attention to the concrete syntax presented along the publications (in fact, Slam-sl specifications are stored as XML files to facilitate interoperability).
Slam-sl is an object oriented formal specification language. Its major characteristics:
