Welcome to the FoCaLiZe website. This site offers information about FoCaLiZe, some documentation about the language and its compiler, some training opportunities, and of course, the latest release of FoCaLiZe.
Welcome to the FoCaLiZe website. This site offers information about FoCaLiZe, some documentation about the language and its compiler, some training opportunities, and of course, the latest release of FoCaLiZe.
The FoCaLiZe project aims at providing a programming environment to develop certified programs. The environment is based on a functional programming language with object-oriented features. The language allows the programmer to write formal specifications and proofs of the program in a unified and consistent setting.
From a FoCaLiZe source code development, the
focalizec compiler produces three source files:
Thanks to built-in inheritance mechanisms, the language allows to refine a development from the coarse-grain specification to the fully defined executable program.
The FoCaLiZe distribution includes a library of mathematical algebraic structures up to multivariate polynomial rings, a library of security policies and various examples contributed by FoCaLiZe users. The resulting libraries are noticeably efficient; for instance, the complex algorithms of the algebraic library provide runtime performances comparable to the best Computer Algebra Systems available.
FoCaLiZe and Zenon are now in two separate GIT repositories. This won't impact the available material but now requires to clone both repositories. This split allows lighter installation when only needing Zenon. Until Zenon's repository is cleanly integrated as a sub-module of the FoCaLiZe one, these two separate clone/pull/push processes are required.
Bugs, feature requests etc. can now be submitted via the FoCaLiZe bug tracker (powered by Bugzilla). We encourage this process instead of direct mails since it allows keeping trace of requests, prevents "memory loss" (the post-it stuck on the screen and finally falling down in the bin or whatever else) and can be used as knowledge database before submitting new requests.
The online version of the tutorial about proofs now contains a section dedicated to explicit induction, i.e. when Zenon does not succeed in finding a proof in a fully automatic way. This section shows how to apply the usual scheme of proof by induction, proving base cases, then induction cases under induction hypotheses.
The new release of the FoCaLiZe environment,
focalize 0.8.0,
is now available. FoCaLiZe got nearly asleep for some years, without
major release despite some underground works. The
"ghost" 0.7.0
version never became public, but the 0.8.0 cumulating the evolutions
of the repository is nearly ready.
Get the last version from the Download page
and the related documentation from the
Documentation page.
After a pretty long time without release, this new version brings number
of enhancements, from the focalizec compiler and
Zenon. New versions of
OCaml and Coq are now supported as well as previous ones for sake of legacy.
Zenon made impressive progress so as to be helpful in proving inductive
properties for species. Installation and setup have been fully revisited,
leading in a simpler and lighter mechanism. The standard library has been
extended with low-level theorems. Termination proofs for structurally
recursive functions are now possible. A certains number of bugs found in the
focalizec compiler have been fixed. And a new tutorial about making proofs
with Zenon is born.
A complete description of changes / new features can in found in the CHANGES
file of the distribution.
The SSURF (Safety and Security UndeR Focal) ANR project was the
starting point of the concretization of the FoCaLiZe environment,
leading to an effective implementation of what is now the focalizec
compiler, greatly helped by Zenon.
As a summary, this project consisted in :
Further information (in french) can be found here.