From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 495C7BBAF; Fri, 7 May 2010 12:39:35 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArINAFaL40uAXTcZ/2dsb2JhbACRVwGMNlcau2WFFQSDYQ X-IronPort-AV: E=Sophos;i="4.52,347,1270418400"; d="scan'208";a="58893611" Received: from deby.inria.fr ([128.93.55.25]) by mail1-smtp-roc.national.inria.fr with ESMTP; 07 May 2010 12:39:26 +0200 Received: by deby.inria.fr (Postfix, from userid 24253) id 2EC7C5A42; Fri, 7 May 2010 12:39:26 +0200 (CEST) To: caml-announce@inria.fr, caml-list@inria.fr, coq-announce@inria.fr, coq-club@inria.fr, coq-list@inria.fr, focalize-users@inria.fr, gdr.gpl@imag.fr Subject: New release of focalize, a development environment for high integrity programs. Message-Id: <20100507103926.2EC7C5A42@deby.inria.fr> Date: Fri, 7 May 2010 12:39:26 +0200 (CEST) From: weis@deby.inria.fr (Pierre Weis) X-Spam: no; 0.00; weis:01 weis:01 camlp:01 coq:01 compiler:01 coq:01 compiler:01 redefinition:01 vastly:01 syntax:01 species:98 species:98 featuring:98 incremental:01 proofs:01 Hi, It is my pleasure to announce the new and second release for FoCaLiZe (the 0.6.0 FoCaLiZe opus). Apart from updating the external tools (Caml, Camlp5 and Coq) this release introduces inductive proofs on the representation of species. Zenon made impressive progress so as to be helpful in proving inductive properties for species. Distributed with this version, we also have a nice tutorial for the language and a set of additional examples. The 0.6.0 release is available from FoCaLiZe.inria.fr at http://FoCaLiZe.inria.fr/download/focalize-0.6.0.tgz Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.6.0 and follow the simple instructions written there. To join people and discussions write to focalize-users@inria.fr. Implementors also listen to suggestions and compliments at mail adress focalize-devel@inria.fr. Enjoy. For the entire FoCaLiZe implementor group, Pierre Weis. Friday, May 7, 2010 10:39:26 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 developped 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 semantices, featuring a rock-solid infrastructure and greatly improved capabilities.