Material disponível ou a disponibilizar:
Bibliografia
- C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition).
(345 pages)
Acetatos
- J.N. Oliveira. Data type invariants: starting where (static) type checking stops (33 slides) (last update: Sep-2014)
- J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (30 slides) (last update: Oct-2014)
- J.N. Oliveira. Specifying functions (32 slides) (Oct-2014)
- J.N. Oliveira. PF transform: when everything becomes a relation (79 slides) (last update: Oct-2014)
- J.N. Oliveira. PF transform: conditions, coreflexives and design by contract (36 slides) (last update: Nov-2014)
- J.N. Oliveira.
Alloy meets the AoP — “Relational thinking” at work (80 slides) (Dec-2014)
NB: Para gerar um
único PDF (4 slides por página) dos acetatos que forem aparecendo acima basta processar o seguinte ficheiro LaTeX:
\documentclass{article}
\usepackage{pdfpages}
\usepackage[landscape]{geometry}
\begin{document}
\includepdf[pages=1-1,nup=1x1]{invariants.pdf}
\includepdf[pages=2-33,nup=2x2]{invariants.pdf}
\includepdf[pages=1-30,nup=2x2]{prepost.pdf}
%includepdf[pages=1-32,nup=2x2]{specfun.pdf}
%includepdf[pages=1-79,nup=2x2]{pftrel.pdf}
%includepdf[pages=1-36,nup=2x2]{pftcond.pdf}
%includepdf[pages=1-80,nup=2x2]{pftalloy.pdf}
% ....... etc .......
\end{document}
(A completar ao longo do curso)
Exemplos, bibliotecas
- Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
- Módulo Alloy: kerimg.als - o que é o núcleo (kernel) e a imagem (image) de uma relação? Experimentem e observem variando a cláusula run.
- Módulo Alloy: agenda.als - o problema genérico de agendamento que generaliza o problema das UCs e perfis do MEI.
Exercícios, formulários etc
Enunciados de provas de avaliação
Divulgação
Ferramentas
Repositórios