Formal Methods: The CAMILA Perspective

J.N. Oliveira

Contents

• Background
• Main Concerns
• The CAMILA/SETS Approach

Background

• Traditional software engineering is admittedly an under-developed branch of Computing Science.
• Structured Programming (1970's), Declarative Programming (1970-80's) and Object-Oriented Programming (1980's) have failed to resolve the ``software crisis''.
• ``Traditional'' Formal Methods are not effective enough.
• Industry has been very slow in adopting formal methods.

Main Concerns

• Simplicity --- industry will never absorve formal methods based on complex mathematical theories.
• Compatibility --- formal methods cannot replace traditional methods altogether.
• Tools --- formal methods should be supported by tools and environments.
• Flexibility --- formal method tools should be easily portable across machine platforms and be able to communicate with existing (traditional) tools.
• Modularity --- or common sense applied to software development; warning: informal modularity is worse than formal monolithic development.
• Reusability --- requires a formal classification scheme; otherwise, repositories are full of things we will never find.
• Back to ``good engineering habits'' --- in school Physics we are taught a universal strategy for problem solving:
  • understand the problem,
  • build a mathematical model of your understanding of it,
  • reason in this model,
  • upgrade your model, if necessary,
  • calculate a solution
  Why don't we do likewise in software development?

The CAMILA/SETS Approach

• Simplicity --- the SETS notation is based on naive set theory, the lambda-calculus and mild use of category theory.
• Compatibility --- traditional notations such as DFDs, ERA-diagrams etc can be inverted to the SETS notation by calculation.
• Life Cycle ---

  

• Tools --- CAMILA is a platform for supporting large-scale development of software using the SETS methodology; the toolkit is still in development but already comprises a rapid-prototyping tool, a structure-editor and a UI semi-automatic generator.
• Flexibility --- the rapid-prototyping tool of the CAMILA environment is available on Unix, MS/DOS and Windows and can be easily interfaced with other tools via C/C++; any CAMILA prototype can be a X-windows server or function like a Windows 3.1 DLL.
• Modularity --- a version of the CAMILA rapid prototyping language is modular and may be based on a repository of software components formally classified using the SETS calculus.
• Reusability --- in a top-down development style, the SETS calculus can be used to horizontally refine a given component and find isomorphic versions of its sub-components in the repository. In a bottom-up style, SETS component aggregation can be expressed by ``software -circuit'' diagrams, using a graphical notation suggestively resembling the conventional hardware notation:

  

  But diagrams should never replace formalisms --- every ``software -circuit'' has a proper semantics and is just a shorthand for some piece of mathematics.

• Back to ``good engineering habits'' --- the SETS reification calculus is used throughout development to calculate possibly distributed solutions (implementations) to specification models.