An Axiomatic Basis for Computer Programming

Um artigo clássico de C. A. R. Hoare, datado de 1969. Esse artigo lançou as bases para provas axiomáticas de corretude de programas e para a semântica axiomática.

O método axiomático foi usado com sucesso na matemática desde que Euclides publicou uma axiomatização da geometria nos seus Elementos. Com o tempo, o método foi aperfeiçoado e hoje é a base de praticamente todas as teorias matemáticas; Aristóteles já chamava a atenção para o fato que uma cadeia de demonstrações deve começar em algum lugar, algumas verdades que são assumidas. Estes são os axiomas.

A tese de Hoare é que é possível estabelecer axiomas básicos para a programação de computadores, e a partir deles, usando regras de inferência também estabelecidas, provar propriedades dos programas, especialmente a sua corretude. Um programa é correto se ele realiza as especificações que foram determinadas para ele, ou seja, se ele faz o que deve fazer. Além disso, os axiomas podem ser utilizado na definição formal de linguagens de programação.

Para exemplificar a plausibilidade do método axiomático na programação, o artigo apresenta alguns axiomas relacionados aos números inteiros e a construções básicas de programação: atribuição, sequenciamento, iteração. Com isso, prova-se que um programa que calcula o máximo divisor comum de dois números é correto, satisfazendo as propriedades matemáticas necessárias para o cálculo.

A seção 5 discute provas de corretude para programas; a idéia, já antiga, de que erros de programação custam caro e que testes nunca podem provar completamente que um programa está correto. Um trecho é interessante:

The practice of supplying proofs for nontrivial programs will not become widespread until considerably more powerful proof techniques become available, and even then will not be easy.

Coisa que até hoje não aconteceu; ainda é trabalhoso demais provar a corretude de programas além dos mais triviais. Entretanto, em alguns casos mais críticos isso já foi feito, principalmente com a ajuda de theorem provers especializados. Muitos microprocessadores também passam por processos de prova formal atualmente; é possível que os métodos formais realizem, um dia, os benefícios visualizados por pioneiros como Hoare e Dijkstra. No artigo, Hoare também menciona como as provas de corretude podem ajudar na documentação e portabilidade de programas.

A seção 6 termina o artigo falando do uso do método axiomático na definição formal de linguagens de programação. Dado que sejam estabelecidos os axiomas e regras de inferência da linguagem, eles servem de definição da própria linguagem: uma implementação só é válida se tornar válidos os axiomas e regras de inferência definidos. Ao mesmo tempo, os axiomas servem automaticamente como base para a prova de corretude da implementação. Hoare fala de Algol 60 e de como a definição formal da sua sintaxe ajudou na formulação de regras sintáticas coerentes, advogando a mesma vantagem para uma definição formal da semântica (tema antigo: simplicidade da definição formal da sintaxe versus complexidade na definição formal da semântica). A semântica axiomática, cuja pesquisa se aprofundou nos anos seguintes, anda meio em desuso, mas os princípios são sólidos.

Faz você pensar no que a computação poderia ser se mais atenção fosse dada às bases teóricas.