Verificação de Programas

A aula de hoje foi minha última aula de Lógica para Computação no 1o. semestre (letivo) de 2012. Foi sobre Verificação de Programas. Os slides usados estão abaixo:

Especificação e Verificação de Programas from Adolfo Neto


 

Verificação de Programas from Adolfo Neto


Além de apresentar os slides, gosto de, durante a aula, mostrar páginas relacionadas ao tema, para ilustrar o assunto.

Alguns dos links foram:

• O que é especificação? por C.A.R. Hoare, em que ele diz que "Uma especificação é apenas um teste generalizado".    Tony Hoare, para quem não sabe, é um dos vencedores do Prêmio Turing. Um Cientista da computação com grandes contribuições.
• Gerard Holzmann é um holandês, criador do SPIN model checker, que atualmente trabalha no JPL da Nasa, um dos principais centros de pesquisa em verificação formal no mundo.
• A página sobre Métodos Formais na Wikipédia lista várias das notações e métodos existentes para fazer especificação e verificação formal.
• Como falo que grandes empresas de desenvolvimento de chips usam verificação formal, encontrei este link da Verificação Formal de um chip ARM.
• O software dos bafômetros dá problema!
• Software dá problema pois temos que escrever na linguagem que o computador entende. Que linguagem é essa? Você pode ter uma ideia lendo este texto sobre a atividade Computador a Papel.
• Não existe computador inteligente! Não existe sistema inteligente!
• Vídeo da visita da turma do PhD Comics ao JPL da Nasa:

Test-Driven Development: Teste e Design no Mundo Real, de Mauricio Aniche - parte 2

Como escrevi em post anterior, estou lendo o livro sobre TDD do Mauricio Aniche.

Terminei hoje de ler os Capítulos 9 e 10.

O Capítulo 9 trata de TDD e Encapsulamento. Segundo Aniche, "encapsular é esconder os detalhes de como a classe realiza sua tarefa; as outras classes devem conhecer apenas o quê ela faz." Encapsulamente sempre foi um dos quesitos principais da Orientação a Objetos (OO). Lembro de textos que li quando OO ainda era novidade nos cursos de graduação em Computação no Brasil (na década de 1990, quando estudei na UFAL) e todos os textos enfatizavam a importância do encapsulamento.

Neste capítulo, Aniche apresenta o exemplo de um Processador de Boletos.  Primeiro apresenta um design com encapsulamento falho, mostra como os testes junto com o conhecimento de design OO indicam esta falha e depois apresenta a correção.

O núcleo do TDD
Fonte: http://www.javacodegeeks.com/2012/05/test-driven-development-win-win.html

 Entre outras coisas, apresenta conceitos como "Tell, Don't Ask", "Lei de Demeter", "intimidade inapropriada", "classes anêmicas". Enfim, aprendi bastante com este capítulo.

O Capítulo 10 é sobre Testes de Integração e TDD. Apresenta o que são Testes de Sistema, Testes de Integração e Testes de Unidade. Discute quando não usar Mocks. Ensina a fazer testes de DAOs. Questiona se devemos usar TDD em Testes de Integração ou em Aplicações Web. Tudo muito bem didático e fácil de entender.
  

Test-Driven Development: Teste e Design no Mundo Real, de Mauricio Aniche

Estou lendo o livro Test-Driven Development: Teste e Design no Mundo Real, de Mauricio Aniche.

Recomendo-o fortemente a todos os interessados em Desenvolvimento de Software.

Ainda não terminei de ler. Estou começando o Capítulo 9. Mas tudo o que já li até agora já foi o suficiente para compensar o investimento de tempo na leitura*.

Por exemplo, o Capítulo 7 trata de TDD e Coesão.

O que é uma classe coesa? Segundo Aniche, "uma classe coesa é justamente aquela que possui apenas uma única responsabilidade."

Os testes que fazemos ao praticar TDD "podem nos avisar sobre problemas de coesão em nossas classes".

Aniche identificou alguns (anti-)padrões na prática de TDD que nos ajudam a encontrar problemas de coesão:

• Muitos Testes Para Um Método
• Muitos Testes Para Uma Classe
• Cenário Muito Grande
• Testes em Método Que Não É Público

Quando um dos padrões acima acontece durante a prática de TDD, é provavelmente hora de refatorar a classe que está sendo testada para melhorar sua coesão. No capítulo, Aniche dá exemplos dos padrões e mostra a solução para os exemplos.

Ao ler o livro, além de aprender sobre TDD você também aprende sobre Orientação a Objetos (e o livro faz referências a textos importantes da área) e sobre Desenvolvimento de Software em geral.

Leia a parte 2.


* Disclaimer: recebi uma cópia para avaliação da Casa do Código.

BRACIS 2012

Participei como voluntário do BRACIS 2012, evento que congrega o SBIA, o SBRN e outros eventos menores.

Como neste momento estou trabalhando pouco com Lógica para Computação (meu foco no momento tem sido Engenharia de Software) não estava tão interessado assim nas palestras do evento. Fui mais como voluntário mesmo para ajudar os professores Myriam, Gustavo e Ernesto, que fazem parte da organização.

Fiquei um pouco decepcionado com o público. Pouquíssima gente (para o que eu esperava). Poucos alunos de graduação.

Um destaque positivo: uma aluna do Doutorado em Engenharia Elétrica e Informática Industrial da UTFPR, Sandra Venske, ganhou um dos prêmios do SBRN (ver imagem abaixo). A orientadora dela, Myriam Delgado, é professora do DAINF e também faz parte do Corpo Docente do PPGCA.

Prêmio recebido por artigo da aluna Sandra Venske, orientanda da a professora Myriam Delgado (DAINF).

Símbolo do BRACIS na camiseta dos voluntários do evento.

PS: o nome deste blog é uma homenagem a este livro.