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.

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)

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

• 'Warm-up exercise' da aula de 25 Set.
• Exercícios sobre caso de estudo "O novo plano de estudos do MEI" previsto para a aula de 4-Dez.

Enunciados de provas de avaliação

Data	Descrição	Ficheiro
07-Jan-2015	Mini-teste	PDF (com a correcção)
28-Jan-2015	Teste	PDF (com a correcção)
12-Fev-2015	Exame de recurso	PDF

Divulgação

• Daniel Jackson. Dependable Software by Design. Scientific American, Junho 2006.

• Leslie Lamport. Why We Should Build Software Like We Build Houses. Wired, 2013.

Ferramentas

• Alloy Analyzer

Repositórios

• Repositório de ferramentas da associação FME.

50 Recent Changes in TWiki Web retrieved at 16:56 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

Benvindo a Especificação e Modelação

Bem vindo à página da edição de 2014/15 da disciplina de Especificação e Modelação do perfil de especialização em Métodos Formais em Engenharia de Software (MFES) do Mestrado em Engenharia Informática da U.Minho. O meu nome é José Nuno Oliveira e sou o docente desta disciplina que, em conjunto com as outras três que prefazem o perfil, ensina uma abordagem científica ao desenvolvimento de software. O perfil MFES é da responsabilidade do Laboratório HASLab (High-Assurance Software Laboratory), em que se vem consolidando know-how em métodos formais de programação desde há três décadas.

Os módulos que compoem MFES corporizam os principais vectores de que depende o projecto de aplicações fiáveis, à escala industrial. Na sua componente teórica, a visão é a de abordar problemas de software segundo uma autêntica perspectiva de engenharia, que permite - através da modelos matemáticos sobre os quais é possível raciocinar e calcular - prever o comportamento dos programas antes de serem escritos.

Especificação e Modelação ensina a conceber e animar modelos de problemas, avaliando-os atempada e exaustivamente antes de se proceder à fase de cálculo e implementação, por forma a evitar erros de perspectiva ou infantilidades de concepção.

Motivação

• Daniel Jackson. Dependable Software by Design. Scientific American, Junho 2006.
• Leslie Lamport. Why We Should Build Software Like We Build Houses. Wired, 2013.

Education/EM Web Preferences

The following settings are web preferences of the Education.EM web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

Web Preferences Settings

These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.

Natural Skin configuration

• Set SKIN=nat

• Set SKINSTYLE = Plain
• Set STYLEBORDER = thin
• Set STYLEBUTTONS = off
• Set STYLESIDEBAR = left
• Set STYLEVARIATION = none
• Set STYLESEARCHBOX = off

• Set PAGETITLE= Especificação e Modelação

• Set NATWEBLOGO = Especificação e Modelação

• Set WEBCOPYRIGHT = Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

• List of topics of the Education/EM web:
  • #Set WEBTOPICLIST = Changes | Index | Search | Go

• Web-specific background color: (Pick a lighter one of the StandardColors).
  • Set WEBBGCOLOR = #D0D0D0
  • Note: This setting is automatically configured when you create a web

• Image, URL and alternate tooltip text of web's logo.
  Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.

• Set WEBLOGOURL = WebHome
• Set WEBLOGOIMG =
• Set WEBLOGOALT = Especificação e Modelação

• List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/EM.Topic links.
  Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
  
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = Especificação e Modelação
  • Set SITEMAPUSETO = Métodos Formais em Engenharia de Software
  • Note: Above settings are automatically configured when you create a web

• Exclude web from a web="all" search: (Set to on for hidden webs).
  • Set NOSEARCHALL =
  • Note: This setting is automatically configured when you create a web

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Education/EM web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW =
  • #Set DENYWEBCHANGE =
  • #Set ALLOWWEBCHANGE = JoseNunoOliveira
  • #Set DENYWEBRENAME =
  • #Set ALLOWWEBRENAME = JoseNunoOliveira

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = TWikiAdminGroup
  • Set ALLOWTOPICRENAME = TWikiAdminGroup

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Web Search

Search: \.*

Tópicos

• Apresentação
• Sumários
• MFES
• Alunos
• Material

Avisos