Agilidade X Formalismo
Sempre vimos o formalismo no desenvolvimento de software como um misto de desejo e desconfiança. Isto é explicável porque se por um lado ele melhora ou mesmo garante a qualidade de uma implementação de software, por outro lado ele costuma implicar em um custo muito alto, exigindo um tempo maior de desenvolvimento e o uso de profissionais com alto grau de formação.
A técnica de prova de corretude que aprendi na universidade foi a do uso da lógica de Hoare – o mesmo que criou o Quicksort, CSP e outros. Nesta técnica, Hoare nos ensinou que cada comando de nosso programa tem uma pré-condição e uma pós-condição que, em resumo, indicam a transformação exercida do comando em nosso ambiente em tempo de execução.
Outro conceito que levei algum tempo para compreender foi a ideia de “invariante”. Para poder indicar o que um loop deve fazer, Hoare nos pedia para definir o ponto-fixo do loop, garantindo que o loop iria convergir para a pós-condição pós-loop.
Complicado? Bem, fica a minha dica para vocês darem uma olhada no vídeo abaixo do time de pesquisa do RiSE. Fica muito mais simples quando temos uma ferramenta de apoio.
Para mim, projetos como este, ou como o Pex e Qex (ambos ferramentas que geram testes a partir de código, seja uma classe ou função, seja uma query SQL), são uma clara indicação de que logo será possível conciliar o desenvolvimento ágil com o rigor formal e o baixo custo.
Se isto acontecer, finalmente poderemos usar sem constrangimentos o termo Engenharia de Software. Sem o cálculo da corretude, ao meu ver, ficamos ainda desmerecedor do termo. Vocês não acham?
PS.: Me desculpem este um mês de ausência, mas as férias me chamavam e não pude resistir. Um grande 2010 para todos!
Comments
Anonymous
January 19, 2010
Olá Otávio, tudo certo? Em resumo, veja se entendi bem... Hoje, a prova formal da corretude de um programa é muito cara. Quando acontece, esse tipo de investimento fica restrito a cenários de programação científica ou em casos especiais, como pesquisa espacial, comandos remotos para hardware especializado, etc. Devido os custos envolvidos, é importante que cada linha de código ou comando seja validado através de lógica formal, como a notação que o Hoare apresentou. No vídeo, o que a Microsoft Reseach está fazendo é criando ferramentas que estarão disponíveis em tempo de desenvolvimento, no próprio Visual Studio no futuro. Isso acontecendo, teremos cenários de mercado, do nosso dia-a-dia, sendo tratados com validações lógicas sem o custo adicional que temos hoje, trazendo um formalismo e uma validação até então restritas ao mundo acadêmico ou grandes investimento. Confere? :) Em tempo, segue abaixo o link para o projeto do specC#, comentado acima: Spec C# Ref.: http://specsharp.codeplex.com/ Abraço! Waldemir.Anonymous
January 19, 2010
Isto :-) Hoje você já pode baixar o spec C# (http://specsharp.codeplex.com/) e já utilizar profissionalmente. Por exemplo: se você tiver um cálculo financeiro complexo e quer garantia formal de que o código implementa a especificação, você pode construir com a ajuda do spec C# a implementação que ele vai te ajudar usando um provador de teoremas que a sua implementação está ok - e isto em tempo de edição ! Depois, você pode retirar as assertivas e invariantes e colocar no C#. Produtividade com qualidade e baixo custo. Abração