Certified Grammar Transformation to Chomsky Normal Form in F
Certified programming allows to prove that the program meets its specification. The check of correctness of a program is performed at compile time, which guarantees that the program always runs as specified. Hence, there is no need to test certified programs to ensure they work correctly. There are...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
Series: | Труды Института системного программирования РАН |
Subjects: | |
Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/64 |
id |
doaj-19d881e5fb4e4087b7436dd483a85a8f |
---|---|
record_format |
Article |
spelling |
doaj-19d881e5fb4e4087b7436dd483a85a8f2020-11-25T02:54:57Zeng Ivannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0128212713810.15514/ISPRAS-2016-28(2)-864Certified Grammar Transformation to Chomsky Normal Form in FM. I. Polubelova0S. N. Bozhko1S. V. Grigorev2Санкт-Петербургский государственный университетСанкт-Петербургский государственный университетСанкт-Петербургский государственный университетCertified programming allows to prove that the program meets its specification. The check of correctness of a program is performed at compile time, which guarantees that the program always runs as specified. Hence, there is no need to test certified programs to ensure they work correctly. There are numerous toolchains designed for certified programming, but F* is the only language that support both general-purpose programming and semi-automated proving. The latter means that F* infers proofs when it is possible and a user can specify more complex proofs if necessary. We work on the application of this technique to a grammarware research and development project YaccConstructor. We present a work in progress verified implementation of transformation of Context-free grammar to Chomsky normal form, that is making progress toward the certification of the entire project. Among other features, F* system allows to extract code in F# or OCaml languages from a program written in F*. YaccConstructor project is mostly written in F#, so this feature of F* is of particular importance because it allows to maintain compatibility between certified modules and those existing in the project which are not certified yet. We also discuss advantages and disadvantages of such approach and formulate topics for further research.https://ispranproceedings.elpub.ru/jour/article/view/64сертификационное программированиеf*верификация программконтекстно-свободная грамматиканормальная форма хомскогопреобразование грамматикиdependent typerefinement type |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
M. I. Polubelova S. N. Bozhko S. V. Grigorev |
spellingShingle |
M. I. Polubelova S. N. Bozhko S. V. Grigorev Certified Grammar Transformation to Chomsky Normal Form in F Труды Института системного программирования РАН сертификационное программирование f* верификация программ контекстно-свободная грамматика нормальная форма хомского преобразование грамматики dependent type refinement type |
author_facet |
M. I. Polubelova S. N. Bozhko S. V. Grigorev |
author_sort |
M. I. Polubelova |
title |
Certified Grammar Transformation to Chomsky Normal Form in F |
title_short |
Certified Grammar Transformation to Chomsky Normal Form in F |
title_full |
Certified Grammar Transformation to Chomsky Normal Form in F |
title_fullStr |
Certified Grammar Transformation to Chomsky Normal Form in F |
title_full_unstemmed |
Certified Grammar Transformation to Chomsky Normal Form in F |
title_sort |
certified grammar transformation to chomsky normal form in f |
publisher |
Ivannikov Institute for System Programming of the Russian Academy of Sciences |
series |
Труды Института системного программирования РАН |
issn |
2079-8156 2220-6426 |
publishDate |
2018-10-01 |
description |
Certified programming allows to prove that the program meets its specification. The check of correctness of a program is performed at compile time, which guarantees that the program always runs as specified. Hence, there is no need to test certified programs to ensure they work correctly. There are numerous toolchains designed for certified programming, but F* is the only language that support both general-purpose programming and semi-automated proving. The latter means that F* infers proofs when it is possible and a user can specify more complex proofs if necessary. We work on the application of this technique to a grammarware research and development project YaccConstructor. We present a work in progress verified implementation of transformation of Context-free grammar to Chomsky normal form, that is making progress toward the certification of the entire project. Among other features, F* system allows to extract code in F# or OCaml languages from a program written in F*. YaccConstructor project is mostly written in F#, so this feature of F* is of particular importance because it allows to maintain compatibility between certified modules and those existing in the project which are not certified yet. We also discuss advantages and disadvantages of such approach and formulate topics for further research. |
topic |
сертификационное программирование f* верификация программ контекстно-свободная грамматика нормальная форма хомского преобразование грамматики dependent type refinement type |
url |
https://ispranproceedings.elpub.ru/jour/article/view/64 |
work_keys_str_mv |
AT mipolubelova certifiedgrammartransformationtochomskynormalforminf AT snbozhko certifiedgrammartransformationtochomskynormalforminf AT svgrigorev certifiedgrammartransformationtochomskynormalforminf |
_version_ |
1724718888591032320 |