A carregar...
Publicação
A Textbook of Verified OCaml Programs. A deductive study on algorithms and data structures
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 1.62 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
We live in a society that has an ever-increasing dependency on critical software.
Even minor programming oversights can have disastrous consequences, ranging from
endangering human and animal lives to economic loss. Thus, it is crucial to verify
the correctness of such programs, which can be achieved with deductive verification
techniques. However, the teaching of such techniques is hampered by the small number
of bibliographical works in this field.
Our goal with this work is ambitious: to write a textbook on verified algorithms and
data structures, fully automated or as close to it as possible. We believe that OCaml is
the perfect programming language choice for this endeavour, due to its multi-paradigm
nature, and its status as a general-purpose language with use cases in both academia
and the industry. And, most importantly, it has good support for automated deductive
verification with Cameleer and GOSPEL.
The current version of the textbook includes more than 1000 lines of verified OCaml
code spread across 6 chapters and more than 40 programs. Moreover, we offer a blend
of functional and imperative case studies, and, overall, a substantial subset of constructs
found in OCaml, including its module system.
In this document, we discuss our thought process and design decisions behind the
creation of a textbook on verified OCaml algorithms. Namely, identifying which classes of
algorithms to tackle, which algorithms were chosen within those classes, and how to orga-
nize the contents of the textbook, to name a few topics. Additionally, this is accompanied
by an overview of theoretical and practical concepts concerning programming languages,
algorithm analysis, deductive verification, and the selected tools.
Vivemos numa sociedade cada vez mais dependente de software crítico. Por menor que um erro de programação possa ser, as suas consequências podem ser desastrosas, desde colocar vidas humanas e animais em perigo até provocar perdas económicas. Por isso, é fundamental garantir a correção de tais programas, o que pode ser efetuado através de técnicas de verificação dedutiva. No entanto, o ensino destas técnicas é dificultado pela escassez de livros científicos nesta área. O nosso objectivo para este trabalho é ambicioso: escrever um livro de algoritmos e estruturas de dados verificadas, de forma totalmente automática ou tão perto disso quanto possível. Acreditamos que OCaml é linguagem de programação perfeita para este efeito. Isto deve-se à sua natureza multi-paradigma e estatuto como linguagem de âmbito geral amplamente utilizada tanto na academia como na indústria. Acima de tudo, porque tem bom suporte para verificação dedutiva automática com Cameleer e GOSPEL. A versão atual deste livro inclui mais de 1000 linhas de código OCaml verificado, distribuídas por 6 capítulos e mais de 40 programas. Para além disso, disponibilizamos uma combinação de casos de estudo funcionais e imperativos. De forma geral, um subconjunto substancial das funcionalidades encontradas em OCaml, incluindo o sistema de módulos. Neste documento, apresentamos a fundamentação e as decisões de design na base da criação de um livro de algoritmos em OCaml verificados. Em particular, identificamos quais as classes de algoritmos a cobrir, quais os algoritmos escolhidos dentro dessas classes, e a forma como os conteúdos do livro estão organizados, entre outros aspetos. Ademais, isto é acompanhado por um resumo dos conceitos teóricos e práticos relativamente a linguagens de programação, análise de algoritmos, verificação dedutiva e as ferramentas selecionadas.
Vivemos numa sociedade cada vez mais dependente de software crítico. Por menor que um erro de programação possa ser, as suas consequências podem ser desastrosas, desde colocar vidas humanas e animais em perigo até provocar perdas económicas. Por isso, é fundamental garantir a correção de tais programas, o que pode ser efetuado através de técnicas de verificação dedutiva. No entanto, o ensino destas técnicas é dificultado pela escassez de livros científicos nesta área. O nosso objectivo para este trabalho é ambicioso: escrever um livro de algoritmos e estruturas de dados verificadas, de forma totalmente automática ou tão perto disso quanto possível. Acreditamos que OCaml é linguagem de programação perfeita para este efeito. Isto deve-se à sua natureza multi-paradigma e estatuto como linguagem de âmbito geral amplamente utilizada tanto na academia como na indústria. Acima de tudo, porque tem bom suporte para verificação dedutiva automática com Cameleer e GOSPEL. A versão atual deste livro inclui mais de 1000 linhas de código OCaml verificado, distribuídas por 6 capítulos e mais de 40 programas. Para além disso, disponibilizamos uma combinação de casos de estudo funcionais e imperativos. De forma geral, um subconjunto substancial das funcionalidades encontradas em OCaml, incluindo o sistema de módulos. Neste documento, apresentamos a fundamentação e as decisões de design na base da criação de um livro de algoritmos em OCaml verificados. Em particular, identificamos quais as classes de algoritmos a cobrir, quais os algoritmos escolhidos dentro dessas classes, e a forma como os conteúdos do livro estão organizados, entre outros aspetos. Ademais, isto é acompanhado por um resumo dos conceitos teóricos e práticos relativamente a linguagens de programação, análise de algoritmos, verificação dedutiva e as ferramentas selecionadas.
Descrição
Palavras-chave
Deductive Verification OCaml GOSPEL Cameleer Why3 Algorithms