{"id":671,"date":"2015-12-30T09:25:09","date_gmt":"2015-12-30T11:25:09","guid":{"rendered":"http:\/\/www.inf.ufrgs.br\/profcomp_wp\/?page_id=671"},"modified":"2016-05-12T16:11:20","modified_gmt":"2016-05-12T19:11:20","slug":"cmp150","status":"publish","type":"page","link":"https:\/\/www.inf.ufrgs.br\/profcomp\/lista-de-disciplinas\/cmp150\/","title":{"rendered":"CMP150"},"content":{"rendered":"<div>\n<h3><strong>M\u00e9todos Formais<\/strong><\/h3>\n<p><b>Respons\u00e1vel<\/b>: <a href=\"http:\/\/www.inf.ufrgs.br\/site\/docente\/daltro-jose-nunes-2\/\">Daltro Jos\u00e9 Nunes<\/a><br \/>\n<b>Pr\u00e9-Requisitos<\/b>: &#8211;<br \/>\n<b>Carga Hor\u00e1ria<\/b>: 60 hs<br \/>\n<b>Cr\u00e9ditos<\/b>: 4<br \/>\n<b>Semestres Oferecidos<\/b>: Primeiro semestre<br \/>\n<b>Matr\u00edcula de Graduandos<\/b>: A matricula dever\u00e1 ser feita como Aluno Especial<br \/>\n<b>P\u00e1gina da Disciplina<\/b>: &#8211;<\/p>\n<p><strong>S\u00daMULA<\/strong><\/p>\n<p align=\"justify\">M\u00e9todos formais, especifica\u00e7\u00e3o formal, prova da especifica\u00e7\u00e3o, prova da implementa\u00e7\u00e3o.<\/p>\n<p><strong>OBJETIVOS<\/strong><\/p>\n<p align=\"justify\">O objetivo da disciplina \u00e9 apresentar os m\u00e9todos formais mais importantes na especifica\u00e7\u00e3o seja de protocolos, de escrit\u00f3rios, de modelos de Banco de Dados, de sistemas operacionais ou de sistemas em geral. Ao final da disciplina o aluno tem condi\u00e7\u00f5es de identificar o problema e escolher um m\u00e9todo formal para apresentar a solu\u00e7\u00e3o (a especifica\u00e7\u00e3o). \u00c9 capaz tamb\u00e9m de verificar a especifica\u00e7\u00e3o, de implementar e de provar a implementa\u00e7\u00e3o contra a especifica\u00e7\u00e3o.<\/p>\n<p><strong>PROGRAMA<\/strong><\/p>\n<p align=\"justify\">M\u00e9todos: Algebrico, VDM, CCS, LOTOS, Z, entre outros<br \/>\nProva da Especifica\u00e7\u00e3o<br \/>\nProva da Implementa\u00e7\u00e3o<\/p>\n<p><strong>CRIT\u00c9RIOS DE AVALIA\u00c7\u00c3O<\/strong><\/p>\n<p align=\"justify\">Os alunos devem estudar um m\u00e9todo formal a sua escolha e apresentar um semin\u00e1rio.<\/p>\n<p><strong>BIBLIOGRAFIA<\/strong><\/p>\n<p align=\"justify\">\u2022 COHEN, B.; HARWOOD, W. T.; JACKSON, M. I. The specification of complex systems. Reading: Addison- Wesley, 1986.<br \/>\n\u2022 GRIES, D. The science of programming. New York: Springer-Verlag, 1981.<br \/>\n\u2022 LOGRIPPO, L.; FACI, M.; HAJ-HUSSEIN, M. An introduction to LOTOS: learning by examples. Computer<br \/>\n\u2022 Networks and ISDN Systems, v. 23, n. 5, p. 325-342, 1992.<br \/>\n\u2022 Especifica\u00e7\u00f5es em Z. ARNALDO VIEIRA MOURA &#8211; Editora Unicamp.<br \/>\n\u2022 The Spec# programming system: An overview. Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. In CASSIS 2004, LNCS vol. 3362, Springer, 2004.<\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>M\u00e9todos Formais Respons\u00e1vel: Daltro Jos\u00e9 Nunes Pr\u00e9-Requisitos: &#8211; Carga Hor\u00e1ria: 60 hs Cr\u00e9ditos: 4 Semestres Oferecidos: Primeiro semestre Matr\u00edcula de Graduandos: A matricula dever\u00e1 ser feita como Aluno Especial P\u00e1gina da Disciplina: &#8211; S\u00daMULA M\u00e9todos formais, especifica\u00e7\u00e3o formal, prova da especifica\u00e7\u00e3o, prova da implementa\u00e7\u00e3o. OBJETIVOS O objetivo da disciplina \u00e9 apresentar os m\u00e9todos formais mais [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":462,"menu_order":150,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/671"}],"collection":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/comments?post=671"}],"version-history":[{"count":3,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/671\/revisions"}],"predecessor-version":[{"id":2512,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/671\/revisions\/2512"}],"up":[{"embeddable":true,"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/pages\/462"}],"wp:attachment":[{"href":"https:\/\/www.inf.ufrgs.br\/profcomp\/wp-json\/wp\/v2\/media?parent=671"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}