Desenho por contrato e verificação de código, uma introdução

Simão Melo de Sousa

Sala 3.4 22 15:15 Esta sessão será dedicada às ferramentas Microsoft para a verificação (da segurança ou da correcção) do código fonte de programas. Assim serão introduzidos os conceitos de lógica de Hoare, desenho por contrato (DbC), verificação estática de contratos assim como os fundamentos e a prática das ferramentas Microsoft que suportam o paradigma DbC (entre outros, Spec#, VCC). Por fim, serão abordados alguns casos práticos de utilização destas ferramentas