FoCaLiZe: Inside an F-IDE
For years, Integrated Development Environments have demonstrated their usefulness in order to ease the development of software. High-level security or safety systems require proofs of compliance to standards, based on analyses such as code review and, increasingly nowadays, formal proofs of conforma...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1404.6607v1 |
| _version_ | 1828159491166699520 |
|---|---|
| author | François Pessaux |
| author_facet | François Pessaux |
| author_sort | François Pessaux |
| collection | DOAJ |
| description | For years, Integrated Development Environments have demonstrated their usefulness in order to ease the development of software. High-level security or safety systems require proofs of compliance to standards, based on analyses such as code review and, increasingly nowadays, formal proofs of conformance to specifications. This implies mixing computational and logical aspects all along the development, which naturally raises the need for a notion of Formal IDE. This paper examines the FoCaLiZe environment and explores the implementation issues raised by the decision to provide a single language to express specification properties, source code and machine-checked proofs while allowing incremental development and code reusability. Such features create strong dependencies between functions, properties and proofs, and impose an particular compilation scheme, which is described here. The compilation results are runnable OCaml code and a checkable Coq term. All these points are illustrated through a running example. |
| first_indexed | 2024-04-12T00:01:51Z |
| format | Article |
| id | doaj.art-84023101a55c4caf98d353ad51d6c27c |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T00:01:51Z |
| publishDate | 2014-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-84023101a55c4caf98d353ad51d6c27c2022-12-22T03:56:12ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-04-01149Proc. F-IDE 2014647810.4204/EPTCS.149.7:2FoCaLiZe: Inside an F-IDEFrançois Pessaux0 ENSTA ParisTech For years, Integrated Development Environments have demonstrated their usefulness in order to ease the development of software. High-level security or safety systems require proofs of compliance to standards, based on analyses such as code review and, increasingly nowadays, formal proofs of conformance to specifications. This implies mixing computational and logical aspects all along the development, which naturally raises the need for a notion of Formal IDE. This paper examines the FoCaLiZe environment and explores the implementation issues raised by the decision to provide a single language to express specification properties, source code and machine-checked proofs while allowing incremental development and code reusability. Such features create strong dependencies between functions, properties and proofs, and impose an particular compilation scheme, which is described here. The compilation results are runnable OCaml code and a checkable Coq term. All these points are illustrated through a running example.http://arxiv.org/pdf/1404.6607v1 |
| spellingShingle | François Pessaux FoCaLiZe: Inside an F-IDE Electronic Proceedings in Theoretical Computer Science |
| title | FoCaLiZe: Inside an F-IDE |
| title_full | FoCaLiZe: Inside an F-IDE |
| title_fullStr | FoCaLiZe: Inside an F-IDE |
| title_full_unstemmed | FoCaLiZe: Inside an F-IDE |
| title_short | FoCaLiZe: Inside an F-IDE |
| title_sort | focalize inside an f ide |
| url | http://arxiv.org/pdf/1404.6607v1 |
| work_keys_str_mv | AT francoispessaux focalizeinsideanfide |