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)

(A completar ao longo do curso)

Acetatos

  • J.N. Oliveira. Data type invariants: starting where (static) type checking stops (32 slides) (last update: Oct-2013)

  • J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (35 slides) (last update: Oct-2013)

  • J.N. Oliveira. PF transform: when everything becomes a relation (66 slides) (last update: Oct-2013)

  • J.N. Oliveira. PF transform: conditions, coreflexives and design by contract (35 slides) (last update: Nov-2013)

  • J.N. Oliveira. Alloy meets the AoP — “Relational thinking” at work (70 slides) (last update: Nov-2013)

  • J.N. Oliveira. “Theorems for free”: a (calculational) introduction (34 slides) (last update: Dec-2013)

  • J.N. Oliveira. PF-transform: using Galois connections to structure relational algebra (79 slides)

  • L. S. Barbosa. Software architecture for reactive systems (introduction) (30 slides)

  • L. S. Barbosa. _Models and logics for reactive systems _ (46 slides)

  • L. S. Barbosa. Introduction to process algebra and the Mu-calculus (54 slides)

  • L. S. Barbosa. Time-critical reactive systems 1 (23 slides)

  • L. S. Barbosa. Time-critical reactive systems 2 (47 slides)

  • L. S. Barbosa. Time-critical reactive systems 3 (32 slides)

  • Three papers on Reo (zip) and modelling exercise Reo (pdf) tinynew.gif

(A completar ao longo do curso)

Outros textos

  • J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Capítulo segundo deste livro em preparação.

(A completar ao longo do curso)

Exercícios e formulários

Trabalhos práticos e avaliações de VFS

Exemplos

(A completar ao longo do curso)

Enunciados de provas de avaliação individual

Divulgação

  • Eric Bouwers, Joost Visser, Arie van Deursen. Getting What You measure. Communications of the ACM (CACM) 55(7):54-59, July 2012.

Ferramentas

Repositórios

Atendimento electrónico (FAQs) tinynew.gif

(Esta secção será actualizada regularmente com as dúvidas mais frequentes que forem colocadas à equipa docente.)

Q1 - (CSI) Não percebi bem a parte final da resolução do exercício 29 feito hoje na aula: para mim, o "sinal maior ou igual" deveria ser "menor ou igual".

R: Vejamos - ter-se-á:

(∀ s,n : s (S . ≤º) n : s (T . S) n)

== { 2 x (41) }

(∀ s,n : (∃ n':: s S n' ∧ n' ≤º n) : (∃ s':: s T s' ∧ s' S n))

== { ≥º = ≤ ; s T s' = true }

(∀ s,n : (∃ n':: s S n' ∧ n' ≥ n) : (∃ s':: s' S n))

O que quer dizer: Se s é o aluno com número n' e n' é maior do que n, então há um aluno s' com o número n (isto é: a alocação de números a alunos é sequencial).


Q2 - (CSI) Tenho dificuldade em decorar a diferença entre núcleo e imagem de uma relação. Há alguma mnemónica que possa ajudar?

R: Haverá concerteza muitas, por exemplo: decore o nome feminino "NEIDE" e leia-o como o acrónimo de "Núcleo, Esquerda, Imagem, Direita, Etc", isto abreviatura de "num núcleo Rº.R o converso está à esqerda, numa imagem R.Rº está à direita, etc". Haverá melhores, mas este já pode ajudar.


Q3 - (CSI) A definição de ordem linear na wikipedia é que são relações transitivas, anti-simétricas e "connected" mas pelo gráfico que nos deu nas aulas são também reflexivas. Qual das duas é a definição correcta?

R: Sendo R "connected" tem-se R ∪ Rº = ⊤ e portanto id ⊆ R ∪ Rº pois id ⊆ ⊤ e ⊤ ⊆ R ∪ Rº.

Ora id ⊆ R ∪ Rº é a mesma coisa que id ∩ (R ∪ Rº) = id e que (por distributividade e conversos) id ∩ R = id, o mesmo que id ⊆ R; logo R é reflexiva.

Em suma, "connected" implica "reflexive", logo não é necessário dizer que é reflexiva.

Usa-se muitas vezes o símbolo ≤ para designar uma ordem linear e o símbolo < para designar ≤ - id, a que se chama a (sub)ordem linear estrita de ≤.


Q4 - Se eu tiver <∀ a,b : a X b : a=b> posso trocar para <∀ a,b : a=b : aXb> e depois aplicar 'one point', correcto?

R: Não (!) Isso é se o quantificador for o existencial (∃). No caso do universal, a troca possível é de <∀ a,b : a X b : a=b> para <∀ a,b :: a X b => a=b>, cf. a regra (7) dos slides para R = true


Q5 - (CSI) A preencher.

R: A preencher.


-- JoseNunoOliveira - 11 Sep 2013