Se você aprendeu métodos formais para software, qual a utilidade?

Se você foi treinado no uso de métodos formais (FM) para programação:

• Quão útil você achou?
• O que envolveu o seu treinamento em FM (por exemplo, um curso, um livro)?
• Quais ferramentas de FM você usa?
• Quais são as vantagens em velocidade / qualidade em comparação com a não utilização de FM?
• Que tipo de software você cria com o FM?
• E se você não usa FM diretamente agora, pelo menos valeu a pena aprender?

Estou curioso para ouvir tantas experiências / opiniões sobre FM quanto essa comunidade; Estou começando a ler e quero saber mais.

fundo

A programação e o desenvolvimento / engenharia de software são algumas das mais recentes habilidades / profissões humanas na Terra; portanto, não é de surpreender que o campo seja imaturo - o que é mostrado na saída principal do nosso campo, como código tipicamente atrasado e propenso a erros. A imaturidade do setor também é mostrada pela ampla margem (pelo menos 10: 1) na produtividade entre os codificadores médios e os principais. Tais fatos sombrios são bem abordados na literatura e apresentados por livros como Code Complete, de Steve McConnell .

O uso de métodos formais (FM) foi proposto pelas principais figuras do software / CS (por exemplo, o falecido E. Dijkstra ) para abordar (uma das) causas principais dos erros: a falta de rigor matemático na programação. Dijkstra, por exemplo, defendia que os alunos desenvolvessem um programa e suas provas juntos .

O FM parece ser muito mais prevalente nos currículos de CS na Europa em comparação com os EUA. Mas nos últimos anos, novas abordagens e ferramentas "leves" de FM, como a Alloy , atraíram alguma atenção. Ainda assim, o FM está longe de ser comum na indústria e espero receber algum feedback aqui sobre o porquê.

Atualizar

Até agora (14/10/2010), das 6 respostas abaixo, ninguém argumentou claramente pelo uso da FM no trabalho "mundo real". Estou realmente curioso para saber se alguém pode e deseja; ou talvez FM realmente ilustre a divisão entre a academia (FM é o futuro!) e a indústria (FM é principalmente inútil).

Absolutamente inútil para qualquer coisa não trivial.

Eu tive um curso chamado, apropriadamente, "Métodos Formais", focado em Alloy - eu não posso ver usando isso em nenhum lugar. Teve outra aula focada na modelagem de simultaneidade com o LTSA - igualmente inútil.

O problema é que a maioria dos erros e problemas de software (pelo menos na minha experiência) surgem da complexidade que ocorre abaixo do nível de abstração dessas ferramentas.

Tenho formação em CSP (Communicating Sequential Processes). Para não me excitar, escrevi minha tese de mestrado sobre o Timed CSP, particularmente "compilando" especificações escritas em métodos formais em C ++ executável. Posso dizer que tenho alguma experiência com métodos formais. Depois de concluir minha graduação e conseguir um emprego na indústria, não utilizo mais métodos formais. Métodos formais ainda são teóricos demais para serem aplicados na indústria. Métodos formais encontraram alguma aplicação prática na área de sistemas embarcados. Por exemplo, a NASA usa métodos formais em seus projetos. Eu especularia que os métodos formais estão muito longe de serem amplamente adotados na indústria. Simplesmente não faz sentido escrever especificações de software em métodos formais e depois "interpretá-las" na sua estrutura de escolha. Inglês simples e diagramas funcionam melhor para isso, enquanto os testes de unidade e integração têm feito um bom trabalho de "verificação" da correção do código. eu acho quemétodos formais permanecerão no mundo da academia por algum tempo .

Diagramas de estado e redes de Petri são úteis para modelar e analisar protocolos e sistemas em tempo real. Primeiro, eles ajudam a projetar uma solução. Segundo, eles ajudam a encontrar casos de teste para softwares interessantes em situações muito específicas.

Eu li alguns livros sobre métodos formais e apliquei alguns. Minha reação imediata foi: "Nossa, esses livros me dizem como ser um bom programador, desde que eu seja um matemático perfeito". Outra fraqueza é que você só pode provar equivalência com outra descrição formal. Escrever uma especificação formal para um programa é o mesmo que escrever um programa em uma linguagem de nível superior, e não há como evitar a introdução de erros em uma especificação razoavelmente grande.

Eu nunca fiz métodos formais funcionarem em grande escala. Eles podem ser úteis para conseguir algo pequeno e complicado, correto, e para me convencer de que estão corretos. Dessa forma, posso trabalhar com blocos de construção um pouco maiores e, às vezes, fazer um pouco mais.

Uma coisa que peguei e que é mais útil em geral é o conceito de invariante, uma declaração sobre um programa e seu estado que é sempre verdadeiro. Tudo o que você pode raciocinar é bom.

Como mencionado acima, eu não sou um matemático perfeito e, portanto, minhas provas às vezes contêm erros. No entanto, na minha experiência, esses tendem a ser grandes erros burros, fáceis de detectar e corrigir.

Fiz um curso de pós-graduação em análise formal de programas, onde nos concentramos na semântica operacional. Fiz meu trabalho final sobre o esforço seL4, revisando os métodos formais que eles usavam. Meu principal ponto de partida em termos de praticidade foi o valor marginal. Você não apenas precisa escrever o programa, mas também a prova. Uau. Duas fontes de erros. Não é só um. Além disso, havia uma enorme quantidade de restrições impostas ao código real. É muito difícil descrever formalmente um computador físico, incluindo E / S.

Autodidata, o TLA +, no ano passado, o utiliza desde então. É uma das primeiras ferramentas que encontro sempre que inicio um projeto. O erro que a maioria das pessoas comete é que elas assumem que os métodos formais são uma coisa do tipo tudo ou nada: ou você não está usando métodos formais ou tem uma verificação completa. No entanto, há algo entre eles: especificação formal , em que você verifica se uma especificação abstrata do seu projeto não quebra seus invariantes. Ao contrário da verificação, a especificação é prática o suficiente para ser usada na indústria.

Linguagens de especificação são mais expressivas que linguagens de programação. Por exemplo, aqui está uma especificação PlusCal (muito) simples para um armazenamento de dados distribuído:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

Esse trecho especifica cinco nós executando simultaneamente, executando transferências em uma ordem arbitrária, em que toda transferência é uma parte arbitrária de dados para um nó arbitrário. Além disso, especificamos que qualquer transferência pode falhar e causar a falha do nó. E podemos simular todos esses comportamentos no verificador de modelos TLA +! Dessa forma, podemos testar se, independentemente de pedidos, taxas de falha etc., nossos requisitos ainda se mantêm. Falando nisso, vamos adicionar alguns requisitos. Primeiro, nunca transferimos dados para um nó offline:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

Em nossa versão simplificada, o verificador de modelo encontrará um estado de falha. Também podemos especificar "qualquer dado dado está em pelo menos um nó online":

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

O que também irá falhar. Boa sorte verificando-os com um teste de unidade!

A principal limitação da especificação é que ela existe independentemente do seu código real. Ele pode apenas dizer que seu design está correto, e não que você o implementou corretamente. Mas é mais rápido especificar do que verificar e captura bugs que são muito sutis para teste, então acho que vale a pena. Praticamente qualquer código envolvendo simultaneidade ou vários sistemas é um bom local para uma especificação formal.

Eu trabalhava em um departamento da ICL, antes de serem compradas pela Fujitsu. Eles tinham alguns contratos grandes do tipo governo que exigiam prova de que o software funcionava conforme anunciado; portanto, eles construíram uma máquina que pegaria a especificação formal escrita em Z e validaria o código enquanto era executado, com uma grande luz verde ou vermelha para aprovação / falhou.

Foi uma coisa incrível, mas, como o estimado @FishToaster aponta, era inútil para qualquer coisa não trivial.

1. " Quão útil você achou? "

A aplicação de redes de Petri à programação de computadores é muito útil. Criei o "Net Elements and Annotations", um método baseado em redes de Petri (Chionglo, 2014). Aplico o método desde 2014 para escrever programas JavaScript que usam a API do Acrobat / JavaScript para aplicativos de formulário PDF.

2. “ O que envolveu seu treinamento em FM (por exemplo, um curso, um livro)? "

Eu "treinei" em redes de Petri através do auto-estudo. Li os capítulos sobre Redes de Petri do livro “Redes de Petri e Grafcet: Ferramentas para Modelagem de Sistemas de Eventos Discretos” (David e Alla, 1992). Também tenho lido artigos de pesquisa sobre redes de Petri. Depois de criar e documentar "Elementos líquidos e anotações", pratiquei a aplicação do método por várias semanas.

3. “ Quais ferramentas de FM você usa? "

Eu desenho diagramas de Petri Net usando o PowerPoint. Eu crio a exibição de formulário das anotações usando o Word. Também crio jogos de token como aplicativos de formulário PDF usando o Acrobat e o Bloco de notas. Depois de adicionar as entradas no formulário, a tradução dessas entradas no código JavaScript é sistemática. Assim, deve ser possível automatizar a tradução. Se as “entradas” foram adicionadas aos objetos gráficos no PowerPoint, também deve ser possível convertê-los sistematicamente em código JavaScript e automatizar também essa tradução. Também uso um conjunto de ferramentas de trabalho em andamento que executa essas traduções e para criar recursos adicionais para a criação de aplicativos de formulário PDF (Chionglo, 2018; 2017).

4. " Que vantagens em velocidade / qualidade você oferece em comparação a não usar FM? "

Posso escrever programas JavaScript usando o "Net Elements and Annotations" mais rapidamente do que posso escrever um programa JavaScript sem usar o "Net Elements and Annotations". E para programas grandes, posso parar de codificar e retornar à codificação mais tarde (ou muito mais tarde) sem me perguntar por onde continuar (Chionglo, 2019). Em alguns casos, posso escrever programas JavaScript usando “Net Elements and Annotations”, mas não consigo gravar os programas JavaScript sem usar “Net Elements and Annotations”. Por exemplo, eu não poderia ter criado implementações não recursivas de funções recursivas sem o uso de "Elementos de rede e anotações" (Chionglo, 2019b; 2018b; 2016). Isso ocorre com ou sem as ferramentas de trabalho em andamento.

5. " Que tipo de software você cria com o FM? "

Uso "Elementos e anotações de rede" para criar programas JavaScript que usam a API do Acrobat / JavaScript para aplicativos de formulário PDF. Também posso aplicar o método para criar programas JavaScript para documentos HTML e para criar esboços do Arduino (Chionglo, 2019c; 2019d).

6. “ E se você não usa o FM agora, vale a pena aprender pelo menos? ” Não aplicável.

Referências

Chionglo, JF (2019b). Computando o nono termo de uma relação recursiva: usando uma função não recursiva - uma resposta a uma pergunta no Mathematics Stack Exchange. < https://www.academia.edu/38496025/Computing_the_N-th_Term_of_a_Recursive_Relation_Using_a_Non-Recursive_Function_A_Reply_to_a_Question_at_Mathematics_Stack_Exchange >.

Chionglo, JF (2019c). Lógica de controle de efeito de chama, simulação e esboço: uma resposta a uma solicitação no fórum da comunidade Arduino. https://www.academia.edu/40342956/Flame_Effect_Control_Logic_Simulation_and_Sketch_A_Reply_to_a_Request_at_the_Arduino_Community_Forum .

Chionglo, JF (2019). Como eu continuo codificando um aplicativo após uma longa pausa? Responda a “Como você sabe onde parou seus códigos após um intervalo de duas semanas?” - Software Engineering Stack Exchange. https://www.academia.edu/39705042/How_I_Continue_Coding_an_Application_after_a_Long_Break_Reply_to_How_do_you_know_where_you_stopped_in_your_codes_after_a_2-week_break_Software_Engineering_StackExchange .

Chionglo, JF (2019d). Lógica de controle Mostrar e ocultar: inspirada por uma pergunta no estouro de pilha. < https://www.academia.edu/40283015/Show-and-Hide_Control_Logic_Inspired_by_a_Question_at_Stack_Overflow >.

Chionglo, JF (2018b). Um modelo de rede de Petri para o fatorial de um número: e uma função JavaScript não recursiva para computá-lo. <>.

Chionglo, JF (2018). Criar Hyper Form ™ - um fluxo de trabalho em andamento: atualização na pesquisa de programação em rede. https://www.academia.edu/37697498/Create_Hyper_Form_-A_Workflow_in_Progress_Update_on_the_Net_Programming_Research .

Chionglo, JF (2017). Programação em rede: uma proposta de pesquisa: para desenvolver aplicativos de formulário PDF com PowerPoint e Acrobat. https://www.academia.edu/33374809/Net_Programming_A_Research_Proposal_For_Developing_PDF_Form_Applications_with_PowerPoint_and_Acrobat. .

Chionglo, JF (2016). Um modelo de rede de Petri para calcular o número de Fibonacci. https://www.academia.edu/31748108/A_Petri_Net_Model_for_Computing_the_Fibonacci_Number.

Chionglo, JF (2014). Elementos de rede e anotações para programação de computadores: cálculos e interações em PDF. https://www.academia.edu/26906314/Net_Elements_and_Annotations_for_Computer_Programming_Computations_and_Interactions_in_PDF .

David, R. e H. Alla. (1992). Redes de Petri e Grafcet: Ferramentas para Modelagem de Sistemas de Eventos Discretos. Sela superior, NJ: Prentice Hall.