Chapter 3: Building certified components within FOCAL

Dubois, Catherine; Hardin, Thérèse; Donzeau Gouge, Véronique Viguié
March 2006
Trends in Functional Programming Volume 5;2006, Vol. 5, p33
Existing provers are good to prove program properties but bad in language support to write large programs. This combination is tackled in the program development environment FOCAL, a framework dedicated to the complete development of certified components, from the specification stage to the implementation one. FOCAL incorporates features such as inheritance, abstraction, late binding and redefinition. The paper gives an overview of the design of the environment and presents the language itself and the associated tools.


Related Articles

  • Chapter 6: Alice Through the Looking Glass. Rossberg, Andreas; Le Botlan, Didier; Tack, Guido; Brunklaus, Thorsten; Smolka, Gert // Trends in Functional Programming Volume 5;2006, Vol. 5, p79 

    We present Alice, a functional programming language that has been designed-with strong support for typed open programming. It incorporates concurrency with data flow synchronisation, higher-ordermodularity, dynamicmodules, and type-safe pickling as a minimal and generic set of simple, orthogonal...

  • Chapter 6: Epigram Reloaded: A Standalone Typechecker for ETT. Chapman, James; Altenkirch, Thorsten; McBride, Conor // Trends in Functional Programming Volume 6;2007, Vol. 6, p79 

    Epigram, a functional programming environment with dependent types, interacts with the programmer via an extensible high level language of programming constructs which elaborates incrementally into Epigram's Type Theory, ETT, a rather spartan λ-calculus with dependent types, playing the...

  • Chapter 5: Static Single Information from a Functional Perspective. Singer, Jeremy // Trends in Functional Programming Volume 4;2005, Vol. 4, p63 

    Static single information form is a natural extension of the well-known static single assignment form. It is a program intermediate representation used in optimising compilers for imperative programming languages. In this paper we show how a program expressed in static single information form...

  • Chapter 4: Type-Specialized Serialization with Sharing. Elsman, Martin // Trends in Functional Programming Volume 6;2007, Vol. 6, p47 

    We present an ML combinator library for serialization, which supports serialization of mutable and cyclic data structures and at the same time preserves sharing. The technique generates compact serialized values, both due to sharing, but also due to type specialization. The library is type safe...

  • The Effect of Pairs in Program Design Tasks. Kim Man Lui; Chan, Keith C. C.; Nosek, John Teofil // IEEE Transactions on Software Engineering;Mar/Apr2008, Vol. 34 Issue 2, p197 

    Pair programming involves two developers simultaneously collaborating with each other on the same programming task to design and code a solution. Algorithm design and its implementation are normally interwoven in that implementation often provides feedback to enhance the design. Previous...

  • Chapter 9: First-Class Open and Closed Code Fragments. Rhiger, Morten // Trends in Functional Programming Volume 6;2007, Vol. 6, p127 

    Multi-stage languages that allow "evaluation under lambdas" are excellent implementation languages for programs that manipulate, specialize, and execute code at runtime. In statically typed multi-stage languages, the existence of staging primitives demands a sound distinction between open code,...

  • On Pattern-Based Programming towards the Discovery of Frequent Patterns. Kerdprasop, Kittisak; Kerdprasop, Nittaya // International Journal of Computer Science;2007, Vol. 2 Issue 4, p268 

    The problem of frequent pattern discovery is defined as the process of searching for patterns such as sets of features or items that appear in data frequently. Finding such frequent patterns has become an important data mining task because it reveals associations, correlations, and many other...

  • Representing Procedural Logic in XML. Bethke, Albert D. // Journal of Software (1796217X);Feb2008, Vol. 3 Issue 2, p33 

    Extensible Markup Language (XML) is a powerful tool used for describing structured documents and exchanging standardized data files over the Internet. This article describes how using XML in an unconventional way greatly improves the usability and effectiveness of an authoring system for...

  • Applications of Symbolic computation in C++ Programming Language. Bakytzhanuly, Satabaldiyev Askar; Nikolayevich, Latuta Konstantin // International Journal of Computer Applications;May2012, Vol. 46, p6 

    This paper contains the brief information about symbolic computation techniques. The location of symbolic computation within Computer Language classification is defined. Programming languages (PL) can be divided into two main areas: imperative PL and declarative PL. Declarative PL is generally...


Read the Article


Sorry, but this item is not currently available from your library.

Try another library?
Sign out of this library

Other Topics