Uma especifica\u00e7\u00e3o formal \u00e9 uma descri\u00e7\u00e3o matem\u00e1tica de software ou de hardware que pode ser utilizada para desenvolver uma implementa\u00e7\u00e3o dos mesmos. Descreve o que sistema deve fazer, e n\u00e3o (necessariamente) como o deve fazer. Dada uma especifica\u00e7\u00e3o, \u00e9 poss\u00edvel utilizar t\u00e9cnicas de verifica\u00e7\u00e3o formal para demonstrar que o modelo de um sistema candidato est\u00e1 de acordo com a sua especifica\u00e7\u00e3o. Isto tem a enorme vantagem de que sistemas candidatos incorrectos s\u00e3o detectados e podem ser revistos antes de se investir na sua implementa\u00e7\u00e3o. Uma aproxima\u00e7\u00e3o alternativa \u00e9 utilizar passos de refinamento para transformar uma especifica\u00e7\u00e3o num modelo completo, e por fim numa implementa\u00e7\u00e3o concreta. \u00c9 importante notar que um modelo (ou implementa\u00e7\u00e3o) nunca pode ser declarado “correcto” isoladamente, mas apenas “correcto no que diz respeito \u00e0 sua especifica\u00e7\u00e3o”. Determinar se uma especifica\u00e7\u00e3o formal descreve correctamente o problema a resolver, \u00e9 um problema \u00e0 parte. \u00c9 tamb\u00e9m um problema de dif\u00edcil resolu\u00e7\u00e3o, uma vez que consiste em construir uma representa\u00e7\u00e3o formal abstracta de um dom\u00ednio de problema informal e concreto, e este passo de abstrac\u00e7\u00e3o n\u00e3o \u00e9 respons\u00e1vel nem suficiente para ser por si s\u00f3 uma prova formal. No entanto, \u00e9 poss\u00edvel validar uma especifica\u00e7\u00e3o provando teoremas relativos \u00e0s propriedades que o sistema deve possuir. Se se verificarem correctos, estes teoremas refor\u00e7am a compreens\u00e3o da especifica\u00e7\u00e3o, e a sua rela\u00e7\u00e3o com o dom\u00ednio do problema. Se n\u00e3o, a especifica\u00e7\u00e3o provavelmente necessita de ser alterada para melhor reflectir a compreens\u00e3o do dom\u00ednio de quem est\u00e1 envolvido na produ\u00e7\u00e3o (e implementa\u00e7\u00e3o) da especifica\u00e7\u00e3o.<\/p>\n","protected":false},"excerpt":{"rendered":"
Uma especifica\u00e7\u00e3o formal \u00e9 uma descri\u00e7\u00e3o matem\u00e1tica de software ou de hardware que pode ser utilizada para desenvolver uma implementa\u00e7\u00e3o dos mesmos. Descreve o que sistema deve fazer, e n\u00e3o (necessariamente) como o deve fazer. Dada uma especifica\u00e7\u00e3o, \u00e9 poss\u00edvel utilizar t\u00e9cnicas de verifica\u00e7\u00e3o formal para demonstrar que o modelo de um sistema candidato est\u00e1 […]<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"closed","template":"","meta":{"wl_entities_gutenberg":"","episode_type":"","audio_file":"","podmotor_file_id":"","podmotor_episode_id":"","cover_image":"","cover_image_id":"","duration":"","filesize":"","filesize_raw":"","date_recorded":"","explicit":"","block":"","itunes_episode_number":"","itunes_title":"","itunes_season_number":"","itunes_episode_type":"","footnotes":""},"categories":[],"wl_entity_type":[43],"class_list":["post-4928","entity","type-entity","status-publish","hentry","wl_entity_type-thing"],"_wl_alt_label":[],"wl:entity_url":"http:\/\/data.wordlift.io\/wl0221\/entity\/especificacao-formal","_links":{"self":[{"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/entities\/4928","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/entities"}],"about":[{"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/types\/entity"}],"author":[{"embeddable":true,"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/comments?post=4928"}],"version-history":[{"count":0,"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/entities\/4928\/revisions"}],"wp:attachment":[{"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/media?parent=4928"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/categories?post=4928"},{"taxonomy":"wl_entity_type","embeddable":true,"href":"https:\/\/semantico.com.br\/blog\/en\/wp-json\/wp\/v2\/wl_entity_type?post=4928"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}