CP/2425

CP 2024/25

Avisos

• 17-Dez: Teste de amanhã, 15h30-17h30 - os alunos devem dirigir-se à sala E1-0.08 e aguardar pela sua distribuição por essa e outras salas.

Avisos anteriores

---

Cálculo de Programas

Bem vindo à página da edição de 2024/25 da unidade curricular de Cálculo de Programas. O principal objectivo desta disciplina é o ensino de métodos que estão na base da abordagem científica ao desenvolvimento de software.

A palavra “programa” vem do grego “programma”, uma derivação de “prographein” = “pro” (antes) + “graphein” (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.

A indústria de software espera das universidades um ensino sistemático da programação, i.e. científico. Só assim haverá garantias de que não há erros de programação. Tal como noutros ramos da engenharia, para isso é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem introduzir erros.

O Departamento de Informática da Universidade do Minho tem uma longa tradição neste tipo de ensino. Com mais de 20 anos de leccionação, Cálculo de Programas é uma das unidades curriculares que ensinam tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores acaba por não ter.

---

Classificação ACM

Conteúdos segundo a taxonomia ACM (5 ECTS no total):

• Software and its engineering/Software creation and management/Software verification and validation/Formal software verification - 1.5
• Theory of computation/Semantics and reasoning/Program reasoning - 2.5
• Theory of computation/Logic/Type theory - 1

---

Funcionamento

Esta UC é dada aos cursos de Engenharia Informática e Ciências da Computação, em dois semestres diferentes.

À parte provas de avaliação, os conteúdos (regime de avaliação, etc) dessas duas edições são exactamente os mesmos.

---

Programa resumido

• Programação composicional: aprender a escrever programas complexos por composição de programas mais simples (princípio da composicionalidade).

• Programação construtiva: aprender a escrever programas funcionais com recurso a combinadores algébricos.

• Transformação de programas: recurso à algebra da programação para se obter eficiência sem sacrifício da correcção.

• Arquitectura da programação: Análise, compreensão e catalogação de programas: recurso à factorização em pares “fold” + “unfold” (hilomorfismos) como forma de se perceber a arquitectura dos algoritmos e sua taxonomia.

• Síntese de programas: cálculo de ciclos-for a partir de definições indutivas da matemática.

• Programação funcional avançada: construir e raciocinar sobre programas funcionais com efeitos sob a forma de mónades.

“Links”

• 40 anos de Métodos Formais na Universidade do Minho) (2024).

• Is abstraction the key to computing? por Jeff Kramer (2007).

• Programming and Maths por Harold Carr (LambdaConf 2015).

• Efeméride: foi em 1978 que o cientista da IBM John Backus publicou o artigo da sua Turing Award - Can Programming be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs - em que declarou as linguagens convencionais incapazes para os desafios que se anunciavam (arquitecturas paralelas), promovendo a programação funcional e iniciando a disciplina da álgebra da programação.

• Haskell na indústria de Software: link