Especificação e Modelação

Métodos Formais em Engenharia de Software

Tópicos

Avisos

23 Fev - Classificações após exame de recurso: serão publicadas em Alunos amanhã.

09 Fev - Por ter faltado, por lapso, a resolução de uma questão do teste de 28-Jan, acrescentou-se essa resolução ao PDF publicado em Material.

08 Fev - Exame de recurso: Sala CPII-208, dia 12-02-2015 (quinta-feira) das 09h00 às 11h00.

08 Fev - Correcção do teste de 28-Jan: está publicada em Material.

05 Fev - Classificações após correcção do teste: estão publicadas em Alunos.

26 Jan - Sala do teste: CPII-201, dia 28-01-2015 (quarta-feira) das 15h00 às 17h00.

19 Jan - Classificações do mini-teste: estão publicadas em Alunos.

19 Jan - Correcção do mini-teste: está publicada em Material.

14 Jan - *Preparação em casa ('Flipped Classroom') da aula de amanhã: estudar o caso de estudo VFS ('Verified File System') e os invariantes 'pc' e 'ri' (228) do respectivo modelo.

06 Jan - Perfil MFES: no final da aula da próxima 5ª-feira (12h) será feita uma breve apresentação dos temas que o perfil MFES tem para oferecer no 2º semestre, na disciplina Laboratório de Engenharia Informática.

06 Jan - Sala do mini-teste: CPII-208, dia 07-01-2015 das 16h00 às 17h00.

14 Dez - O mini-teste de 7-Jan (16h-17h, com consulta) constará de 4 questões (cada uma valendo 2.5 valores) e versará sobre toda a matéria até ao exercício 57, inclusivé.

14 Dez - 'Flipped Classroom' para 18 Dez : estudar os exercícios 47, 48, 56 e 57.

11 Dez - Mini-teste: 7-Jan, das 16h às 17h, sala e matéria a indicar.

09 Dez - (Anúncio) Bolsa BIL 6 meses em Programação funcional avançada : eventuais alunos desta disciplina interessados devem contactar o docente da disciplina ou o Prof. M.M. Barbosa (mbb@di.uminho.pt) até à próxima quinta-feira o mais tardar.

06 Dez - 'Flipped Classroom' para 11 Dez : estudar os exercícios 64, 67 e 68.

29 Nov - 'Flipped Classroom' para 04 Dez : estudar cuidadosamente a ficha Exercícios sobre caso de estudo "O novo plano de estudos do MEI" que está prevista para essas aulas.

22 Nov - 'Flipped Classroom' para 27 Nov : estudar a prova de (79) (anexo dos slides) e os exercícios 40 e 52.

14 Nov - 'Flipped Classroom' para 20 Nov : fazer os exercícios 49, 50, 51, 53 e 54.

10 Nov - No próximo dia 13-Nov vai haver uma aula TP suplementar de EM no horário de ATS (resolução de exercícios).

10 Nov - 'Flipped Classroom' para 13 Nov : fazer os exercícios 44 e 45; derivar a versão PF do invariante do "problema MEI" da aula anterior.

05 Nov - As aulas desta disciplina regressam a partir de hoje à sala DI-0.03.

01 Nov - 'Flipped Classroom' para 6 Nov : fazer os exercícios 31, 33, 34 e 36.

24 Out - 'Flipped Classroom' para 30 Out : (a) fazer os exercícios 25, 26, 27, 29 e 31; (b) completar o modelo 'Propositio de homine et capra et lvpo' em Alloy com factos (slide 35) e correr no Alloy analyser.

22 Out - As aulas desta disciplina passam a partir de hoje a ter lugar na sala DI-0.05.

15 Out - As aulas desta disciplina passam a partir de hoje a ter lugar na sala DI-0.03.

23 Set - As aulas iniciam-se no próximo dia 25 de Setembro, às 9h00, na sala DI 1.08.

22 Set - Criação do site.

Education » EM » WebHome » Material

Material disponível ou a disponibilizar:

Bibliografia

D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

J.N. Oliveira. Extended static checking by calculation using the pointfree transform. In A. Bove et al., editor, volume 5520 of LNCS, pages 195-251. Springer-Verlag, 2009.

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)