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.
Proofs are written in a hierarchical style in the FoCaLiZe Proof
Language and are then independent from the target logical verification
system. Leaves of a proof tree are solved by providing "hints"
(definition, theorem, proof step etc. names) which are sent to the
Zenon automatic theorem prover.
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 is developped by François Pessaux. Zenon is developped by Damien
Doligez.
The new release of the FoCaLiZe environment,
focalize 0.9.5,
is now available.
After being broken for a long time due to changes in OCaml and
Coq, this version is now compatible with the recent versions
of OCaml (5.0.0) and Coq (8.17.0). As a side
effect, this makes FoCaLiZe available on Mac Silicon (M1/M2).
The distribution is available from the dedicated
GitHub repository.
The new release of the FoCaLiZe environment,
focalize 0.9.2,
is now available.
As for previous releases, some bugs have been fixed in the
focalizec compiler.
This version introduces the Dedukti backend written by
Raphaël Cauderlier, taking benefits from Zenon_modulo to
ease proofs.
The Coq backend now generates Coq code compatible with Coq 8.8.
A complete description of changes / new features can in found in the CHANGES
file of the distribution.
FoCaLiZe git repository moved to GitHub. You may find the project page and clone the repository from https://github.com/pessaux-f/focalize.git.
A currently short but growing FAQ about common errors is now available from the Documentation page.
Bugs have been fixed for proofs using definitions of recursive functions, and some proofs using congruence-related mechanisms. This version is available from its GIT repository or Zenon website.
A minor change in Zenon installation process allowing to
handle Coq 8.5 has been made. This version is available from its GIT
repository or Zenon website.
The new release of the FoCaLiZe environment,
focalize 0.9.1,
is now available.
A certain number of bugs found in the focalizec compiler have
been fixed.
The generated code is slightly lighter. Termination proofs for recursive
functions, in addition to the previously available structural way, can be now
written using a measure or a well-founded relation.
The generated Coq code is now compatible with Coq 8.5, but whoever requires
Zenon 8.0.1 (or to configure its installation to store the
libraries in a dedicated directory).
A complete description of changes / new features can in found in the CHANGES
file of the distribution.
The GIT repositories of FoCaLiZe and Zenon are now daily mirrored at ENSTA. We hope that the synchronization will work fine...
The new release of the FoCaLiZe environment,
focalize 0.9.0,
is now available.
A certain number of bugs found in the focalizec compiler have
been fixed and Zenon also had several issues fixed.
Final let-definitions are now integrated. The computation of
dependencies has been deeply rewritten to compute them *once* for all the
possible backends (OCaml, Coq). Generated code is slightly lighter and
naming schemes and code generation schemes have been standardized between
OCaml and Coq.
A complete description of changes / new features can in found in the CHANGES
file of the distribution.
Due to an issue on the old server hosting FoCaLiZe, the site was down during some weeks. The situation is now back to a normal state after a migration. Only the bugtracker is still down and will be fixed soon.
The material of the course given at Ecole des Jeunes Chercheurs en Programmation (EJCP) in May 2014 is now available via the Documentation page. This document introduces the aims of proving software and shows application using FoCaLiZe.
The tutorial "Playing with Proofs" available in the distribution and via the Documentation page has been updated to make the proof dealing with tree mirror working again. We still have to add few words to explain clearly how to state induction hypotheses in case of multiple recursive calls. Some words also have to be added about the shape of the goals and the equivalent shapes they can have to allow Zenon to use induction. Will be done ASAP ;)
Due to a site migration, some links to papers available in the Resources page got broken. The PDF files are now back.
final let-definitions available (2014-01-31)
A new feature is now available (currently only from the GIT repository)
allowing to forbid redefinitions of let-definitions (logical or not): the
final qualifier.
This feature was requested to avoid duplicating the code of a logical let
by adding a theorem paraphrasing the definition's body in order to prevent
further redefinitions from changing the definition.
For sake of homogeneity, "final-ity" is available also for "non-logical"
definitions.
The following code*:
logical let is_A_singleton = all a : A, A!equal (a, A!element);
(* Theorem to avoid changes of is_A_singleton. *)
theorem is_A_singleton_spec :
is_A_singleton <-> all a : A, A!equal (a, A!element)
proof = by definition of is_A_singleton ;
may now be simplified in:
logical final let is_A_singleton = all a : A, A!equal (a, A!element);
Since no children in the inheritance will be allowed to alter the "meaning"
of is_A_singleton, the theorem is_A_singleton_spec
is no more needed.
(*) Thank's to Mathieu and Théo for the example.
Zenon GIT repository got corrupted
causing an incorrect
git clone when used as anynymous user via the http link
provided in the Download page. The version that was
fetched did not include number of (more or less) recent commits, hence did
not make available bug fixes and features of Zenon.
This is now fixed, users can clone or update their version of Zenon.
Versions prior to 0.7.2 [a257] 2014-01-05 are out-of-date
and were possibly impacted by the repository corruption.
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.