From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 6FA5B7FDE2 for ; Mon, 30 May 2016 13:56:57 +0200 (CEST) IronPort-PHdr: 9a23:Zb7buRb5GFK9lF+MxGtHmIL/LSx+4OfEezUN459isYplN5qZpcqybnLW6fgltlLVR4KTs6sC0LqH9f27EjBcqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0psaYP1kArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8xSLgdCDU9Lyhh78TusVzHTBCTznoaSGQf1BRSVVvr9hb/C7nruy11setm7xGXJtb/UKB8DTq45qFgTx7zzj8KLCUw7XH/h8prkKseuBu7pgdjzoXUJo+PYqktNpjBdM8XEDISFv1aUDZMV9ux Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=francois.pessaux@ensta-paristech.fr; spf=Pass smtp.mailfrom=francois.pessaux@ensta-paristech.fr; spf=Pass smtp.helo=postmaster@ns4.ensta.fr Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of francois.pessaux@ensta-paristech.fr) identity=pra; client-ip=147.250.10.4; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="francois.pessaux@ensta-paristech.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of francois.pessaux@ensta-paristech.fr designates 147.250.10.4 as permitted sender) identity=mailfrom; client-ip=147.250.10.4; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="francois.pessaux@ensta-paristech.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@ns4.ensta.fr designates 147.250.10.4 as permitted sender) identity=helo; client-ip=147.250.10.4; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="francois.pessaux@ensta-paristech.fr"; x-sender="postmaster@ns4.ensta.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0B9AQA6KUxXdgQK+pNdhBJ9g0OuY4JghH4BDYF5IocfOBQBAQEBAQEBAREBDBQJUIIwgj9PZAJfE4gvBQmabY9ikTeCJIV6hnkBAYMkK4IuBYgEizOFAIYAgTGGb4FpTocKI4U4j0oCDw8BAYIEgi1sAQEBiAWBNQEBAQ X-IPAS-Result: A0B9AQA6KUxXdgQK+pNdhBJ9g0OuY4JghH4BDYF5IocfOBQBAQEBAQEBAREBDBQJUIIwgj9PZAJfE4gvBQmabY9ikTeCJIV6hnkBAYMkK4IuBYgEizOFAIYAgTGGb4FpTocKI4U4j0oCDw8BAYIEgi1sAQEBiAWBNQEBAQ X-IronPort-AV: E=Sophos;i="5.26,389,1459807200"; d="scan'208,217";a="179467152" Received: from ns4.ensta.fr ([147.250.10.4]) by mail3-smtp-sop.national.inria.fr with ESMTP; 30 May 2016 13:56:56 +0200 Received: from ns4.ensta.fr (localhost [127.0.0.1]) by ns4.ensta.fr (Postfix) with ESMTP id 3C809F84B2 for ; Mon, 30 May 2016 13:56:56 +0200 (CEST) X-Virus-Scanned: amavisd-new at ns4.ensta.fr Received: from ns4.ensta.fr ([127.0.0.1]) by ns4.ensta.fr (ns4.ensta.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id v64B_lkuwwdh for ; Mon, 30 May 2016 13:56:53 +0200 (CEST) Received: from zemail.ensta.fr (zemail.ensta.fr [147.250.1.16]) by ns4.ensta.fr (Postfix) with ESMTP id 86D83F84A4 for ; Mon, 30 May 2016 13:56:53 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id 835FD29723B for ; Mon, 30 May 2016 13:56:53 +0200 (CEST) Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10032) with ESMTP id QBtSuFUpFCid for ; Mon, 30 May 2016 13:56:52 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by zemail.ensta.fr (Postfix) with ESMTP id AF1EF297C52 for ; Mon, 30 May 2016 13:56:52 +0200 (CEST) X-Virus-Scanned: amavisd-new at zemail.ensta.fr Received: from zemail.ensta.fr ([127.0.0.1]) by localhost (zemail.ensta.fr [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id 7WqrDy13ef_m for ; Mon, 30 May 2016 13:56:52 +0200 (CEST) Received: from [147.250.223.18] (unknown [147.250.223.18]) by zemail.ensta.fr (Postfix) with ESMTPSA id 90BFF29723B for ; Mon, 30 May 2016 13:56:52 +0200 (CEST) From: =?utf-8?Q?Fran=C3=A7ois_Pessaux?= Content-Type: multipart/alternative; boundary="Apple-Mail=_34874AC9-2BD8-42CA-8B42-E5F9BD855AF2" Message-Id: Date: Mon, 30 May 2016 13:56:52 +0200 To: caml-list Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) X-Mailer: Apple Mail (2.3124) Subject: [Caml-list] FoCaLiZe 0.9.1 released --Apple-Mail=_34874AC9-2BD8-42CA-8B42-E5F9BD855AF2 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 It is my pleasure to announce the new release for FoCaLiZe (the 0.9.1 version). 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 n= ow written using a measure or a well-founded relation. A complete description of changes / new features can in found in the CHANGES file of the distribution. The 0.9.1 release is available from focalize.inria.fr at http://focalize.inria.fr/download/focalize-0.9.1.tgz Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.9.1 and follow the simple instructions written there. A public GIT repository is also available, allowing to fetch the latest development state of FoCaLiZe. However, its content is not bullet-proof and may be unstable at some times. It reflects the real-time state of FoCaLiZe and may bring fixes and features not available in previous releases and that will be part of the next release. To clone the current FoCaLiZe GIT repository, invoke: git clone http://focalize.inria.fr/focalize.git This will create a focalize repository in your current directory. Once clon= ed, it is possible to fetch updates with the usual GIT commands (essentially git pull origin master). Note that this access being public, it doesn't allow pushing (i.e. submitting) modifications done in the sources tree. To join people and discussions write to focalize-users@inria.fr. Implementors also listen to suggestions (and compliments if some ^_^) at the mail address: focalize-devel@inria.fr. Enjoy. For the entire FoCaLiZe implementation group, Fran=C3=A7ois Pessaux. May 2016 What is it FoCaLiZe ? --------------------- FoCaLiZe is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLiZe provides a logical framework to express the properties of the code. A simple declarative language provides the natural expression of proofs of properties them from within the program source code. The FoCaLiZe compiler extracts statements and proof scripts from the source file, to pass them to the Zenon proof generator to produce Coq proof terms that are then formally verified. The FoCaLiZe compiler also generates the code corresponding to the program as an Objective Caml source file. This way, programs developed in FoCaLiZe can be efficiently compiled to native code on a large variety of architectures. Last but not least, FoCaLiZe automatically generates the documentation corresponding to the development, a requirement for high evaluation assurance. The FoCaLiZe system provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation, while proving that their implementation meets its specification or design requirements. The FoCaLiZe language offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically generated ultimately relies on Coq formal proof verification. FoCaLiZe is a son of the previous Focal system. However, it is a completely new implementation with vastly revised syntax and semantics, featuring a rock-solid infrastructure and greatly improved capabilities. --Apple-Mail=_34874AC9-2BD8-42CA-8B42-E5F9BD855AF2 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 
It=
 is my pleasure to announce the new release for FoCaLiZe (the
0.9.1 version).

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 n=
ow
written using a measure or a well-founded relation.
A complete description of changes / new features can in found in the CHANGES
file of the distribution.

The 0.9.1 release is available from focalize.inria.fr at
http://focalize.inria.fr/download/focalize-0.9.1.tgz
Uncompress, extract, then read the INSTALL file in the newly created
directory focalize.0.9.1 and follow the simple instructions written there.


A public GIT repository is also available, allowing to fetch the latest
development state of FoCaLiZe. However, its content is not bullet-proof and
may be unstable at some times. It reflects the real-time state of FoCaLiZe
and may bring fixes and features not available in previous releases and that
will be part of the next release.
To clone the current FoCaLiZe GIT repository, invoke:
   git clone h=
ttp://focalize.inria.fr/focalize.git
This will create a focalize repository in your current directory. Once clon=
ed,
it is possible to fetch updates with the usual GIT commands (essentially git
pull origin master). Note that this access being public, it doesn't allow
pushing (i.e. submitting) modifications done in the sources tree.


To join people and discussions write to focalize-users@inria.fr.
Implementors also listen to suggestions (and compliments if some ^_^) at the
mail address: focaliz=
e-devel@inria.fr.

Enjoy.

For the entire FoCaLiZe implementation group,

Fran=C3=A7ois Pessaux.

May 2016

What is it FoCaLiZe ?
---------------------

FoCaLiZe is an integrated development environment to write high integrity
programs and systems. It provides a purely functional language to formally
express specifications, describe the design and code the algorithms.
Within the functional language, FoCaLiZe provides a logical framework to
express the properties of the code. A simple declarative language provides
the natural expression of proofs of properties them from within the program
source code.

The FoCaLiZe compiler extracts statements and proof scripts from the source
file, to pass them to the Zenon proof generator to produce Coq proof terms
that are then formally verified.

The FoCaLiZe compiler also generates the code corresponding to the
program as an Objective Caml source file. This way, programs developed in
FoCaLiZe can be efficiently compiled to native code on a large variety of
architectures.

Last but not least, FoCaLiZe automatically generates the documentation
corresponding to the development, a requirement for high evaluation
assurance.

The FoCaLiZe system provides means for the developers to formally express
their specifications and to go step by step (in an incremental approach) to
design and implementation, while proving that their implementation
meets its specification or design requirements. The FoCaLiZe language offers
high level mechanisms such as inheritance, late binding, redefinition,
parametrization, etc. Confidence in proofs submitted by developers or
automatically generated ultimately relies on Coq formal proof verification.

FoCaLiZe is a son of the previous Focal system. However, it is a completely
new implementation with vastly revised syntax and semantics, featuring a
rock-solid infrastructure and greatly improved capabilities.

= --Apple-Mail=_34874AC9-2BD8-42CA-8B42-E5F9BD855AF2--