Home

capítulo 3 métodos formais

1. bem como pelos esfor os de Parnas Parnas 72 no sentido de que a modularidade dos progra mas fosse baseada em unidades de implementa o suportadas pelas lingua gens de programa o promovendo o isolamento das 19 baseadas em modelos matem ticos 20 Na g nese da tecnologia orientada aos objectos CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 84 representa es em conjun to com as respectivas opera es de acesso encapsulamento bem como a sua opacidade exterior ou seja a impossibilidade do utilizador da unidade ter acesso representa o interna dos dados information hidding Tal acesso seria apenas permitido atrav s de uma interface bem definida constitu da pelo conjunto das opera es implementadas que explicitamente fossem tornadas p blicas pelo implementador do m dulo quaisquer que fossem os mecanismos encontrados pelas linguagens para tal Estas unidades de encapsulamento com tais caracter sticas de acesso s o genericamente designadas por mecanismos de abstrac o de dados2 por analogia com os j existentes mecanismos de abs trac o de controlo cf procedimentos e fun es As solu es encontradas pelas diversas linguagens de programa o para tal tipo de requisitos foram diversas cabendo referir aqui sem refer ncias as solu es que foram encontradas nas linguagens de programa o mais popularizadas tais como UCSD Pascal units Modula 2 modules CLU clusters e Ada pac
2. len initg O tem comprimento zero empty initq true n o tem elementos 29 closure 30 O s mbolo utilizado uma simplica o do verdadeiro valor de erro que deveria ser associado esp cie do termo Assim a cada esp cie um termo de erro deveria ser associado A complexidade da sem ntica de erro de desnecess ria introdu o aqui tratada por exemplo em Ehrig e Mahr 85 CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 91 Em alguns casos axiomas condicionais devem ser considerados j que o significado da opera o pode ser dependente do contexto em que a mesma executada No exemplo o axioma condicional first enqueue g e empty q e empty q first q indica duas poss veis igualdades ou seja duas poss veis interpreta es do ter mo first enqueue q e a primeira num contexto em que a fila de espera se en contra vazia situa o particular em que o elemento inserido passa a coincidir com o primeiro da fila e a segunda onde por n o se encontrar a fila vazia a propriedade apresentada apenas garante que o primeiro elemento da nova fila continua a ser o elemento que era o primeiro da fila antes da altera o desta ou seja que a inser o n o foi feita no topo mas na cauda dada a intui o de que uma fila uma estrutura linear com dois extremos para opera o Esta concentra o do m todo no comportamento observ vel atrav s de um conjunto de propriedade
3. os desenvolvidos por forma a que a concep o e o desenvolvimento de programas em particular e a Engenharia da Programa o em geral possuam uma base de rigor indiscut vel e t o necess ria Na apresenta o caminha se da sem ntica das linguagens eta pa b sica para que programas possam ter significado para os m todos formais de concep o e desenvolvimento que dever o possibilitar o estabelecimento de contextos rigorosos para que os programas possam ser desenvolvidos em con cord ncia com as suas especifica es de forma integrada e provadamente cor recta 3 2 1 Sem ntica das Linguagens A possibilidade de se realizarem racioc nios e provas matem ticas sobre a correc o de programas de computador foi uma preocupa o imediata dos principais pioneiros da computa o cf Goldstine e von Neumann 47 Turing 49 posteriormente retomados por outros investigadores da rea McCarthy 63 van Wijngaarden 66 Naur 66 e Floyd 67 ainda que muitos dos resulta dos obtidos n o tenham sido imediatamente relacionados entre si e consequen temente refor ados por serem resultantes de esfor os individuais Por m a verifica o da correc o dos programas i a possibilidade de se produzirem argumentos sobre a sua correc o n o pode ser desligada do signi ficado sem ntica das diversas constru es sint cticas da linguagem CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 71 em que estes s o esc
4. veis elementos do tipo em defini o Por exemplo no caso do TAD Queue todos os poss veis valores de uma queue podem ser modelados por express es que envolvem sucessivas aplica es da opera o enqueue ao valor inicial representado por initg Por exemplo em Queue Nat i filas de naturais ter amos representa es de queues sob a forma enqueuelinitq 10 enqueue enqueuefinitg 10 15 enqueue enqueue enqueue initg 10 15 27 Os interrogadores ou observadores s o os operadores definidos cujo resul tado de uma esp cie primitiva Assim estes operadores permitem especificar a sem ntica dos construtores e tamb m dos modificadores por observa o em l gebras mais primitivas No exemplo apresentado as opera es first empty e len s o exemplos de interrogadores pois n o d o como resultado qualquer representa o de um objecto da esp cie queue mas antes de objectos de esp cies primitivas sejam elas esp cies par metro ou n o Finalmente surgem os operadores semantica mente mais importantes os modificadores Designam se por modificadores todos os operadores que se aplicam a termos da esp cie principal e d o como resulta do outros termos da esp cie principal correspondendo assim simbolicamente a uma transi o de estado do objecto de interesse assim representado No exem plo os operadores dequeue e enqueue s o os nicos modificadores dado que s o os nicos que aplicados a
5. 60 SUMA Orar espionar deal a DOSE Da a EA Eca ba a 105 CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 66 3 1 Introdu o Ainda que a hist ria da evolu o de uma rea cient fica ou disciplina seja de ineg vel interesse para a compreens o do seu estado actual e tal esteja por fazer com rigor e detalhe relativamente Ci ncia da Computa o n o se pretende realizar nesta sec o tal tarefa mas t o s apresentar em s ntese alguns dos marcos da evolu o considerados pelo autor como importantes para a compreens o das raz es do aparecimento dos formalismos e m todos formais ou rigorosos de descri o e especifica o de programas bem como dos desideratos que justificam a adop o dos mesmos A primeira e bem reconhecida crise da Programa o de Computadores surge nos anos 60 resultante de tr s factores capitais o aparecimento de uma nova gera o de computadores de maior capacidade o normal incremento da comple xidade dos problemas a resolver em resultado de um aumento das expectati vas a incapacidade metodol gica e tecnol gica sentida data para tratar problemas de tal complexidade tamb m neste per odo que os computadores passam definitivamente do mbito das m quinas de c lculo para o contexto mais universal de m quinas de tratamento simb lico e de processamento de dados Sentiu se ent o a designada crise l gica dos anos 60 e em resultado uma generalizada mobiliza o d
6. Martins 90 3 3 M todos Formais 21 data abstractions 22 haveria que distinguir dentre os mecanismos que possibilitam a cria o de tipos definidos pelo utilizador os que se baseiam em mera exporta o e os que s o verdadeiros construtores detipos 23 abstract data type ADT CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 85 3 3 1 M todos Formais Motiva o O software indiscutivelmente um produto singular N o feito a partir de materiais em bruto antes sendo um derivado do pr prio processo subjacente sua concep o e realiza o Assim sendo o software um produto de qualidade ligada quase exclusivamente ao processo dado n o ser constru do com kase em mat rias primas preocupante que os processos ainda hoje empregues no desenvolvimento de programas primem pela quase total aus ncia de rigor e for malidade N o portanto de estranhar que muita da nfase colocada no projecto de software se situe exactamente no processo suas fases seus custos normais seus erros custos dos erros rigor etc Tratando se de um problema intr nseco ao desenvolvimento e qualidade do produto final a aplica o de m todos formais na captura de requisitos e no desenvolvimento uma decis o metodo l gica inteiramente do foro e do interesse da equipa de projecto O utilizador v o produto final mede a sua qualidade geral mas n o se apercebe nem discute o processo segundo o qual o m
7. das v rias opera es e a sem ntica do sistema espe cificada usando axiomas que relacionam opera es entre si Por m quando a complexidade de um sistema grande apesar da modularidade permitida na maior parte dos sistemas de especifica o alg brica o n mero de axiomas pode tornar se bastante grande Os m todos baseados em modelos matem ticos surgem como alternativa aos m todos alg bricos Nestes m todos que trazem at ao software uma larga tra di o em ci ncias exactas e de engenharia uma especifica o um modelo ma tem tico expl cito do sistema Este modelo constitu do pelos seguintes compo nentes uma associa o de um tipo matem tico dentre os definidos pelo m to do a cada esp cie de objectos do sistema passando a ser o seu mo delo abstracto matem tico na especifica o a identifica o de um estado interno do sistema tamb m modelado por um tipo matem tico sendo sobre o conjunto dos seus valores v lidos que se especificam as opera es definidas cada opera o de interroga o ou observa o do sistema especifi cada como uma fun o matem tica sem efeitos laterais contudo permitem se tamb m opera es que para al m de poderem alterar o estado podem tamb m produzir resultados sendo os argumentos destas opera es os tipos matem ticos definidos como modelos dos tipos do sistema tais opera es s o especificadas como rela es ma tem ticas envolvendo
8. de computador escritos usando linguagens de progra ma o torna se ent o bvio que a sem ntica de um programa est intrinseca mente ligada pr pria sem ntica das constru es da linguagem em que est escrito Logo fundamental que as linguagens de programa o sejam dotadas de sem ntica rigorosa Por outro lado programas s o constitu dos por dados e por entidades que manipulam tais dados em particular no modelo convencional imperativo Assim a sem ntica de uma linguagem deve dar significado a uns e a outros o que ao longo do tempo nem sempre aconteceu de modo equilibrado Finalmente a correc o de um programa est estreitamente ligada satisfa o por parte deste de um conjunto de requisitos dos quais os requisitos funcionais t m merecido uma particular aten o A correc o funcional de um programa apenas pode ser determinada caso o significado funcional deste puder ser confrontado com os requisitos funcionais para o mesmo definidos Idealmente o significado do programa e dos requisitos seria estabelecido de modo rigoroso num contexto matem tico desta forma possibilitando uma prova matem tica Por m por raz es que se apresentam a seguir relacionadas com as dificuldades de se estabelecerem significados mate m ticos rigorosos quer para programas quer para especifica es a pr tica mais corrente vai no sentido da utiliza o de m todos informais Apresentam se nas sec es seguintes os diversos esfor
9. e um dom nio sem ntico fun o que tradi cionalmente representada por par nteses rectos duplos o Dom nio Sint ctico Dom nio Sem ntico 10 Tradu o comum do original denotation 11 cf meaning functions 12 cf semantic domains CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 76 O esquema de tradu o apresentado na figura 3 8 Programa Fun o Significado Denota o Fig 3 3 Sem ntica Denotacional A sem ntica operacional funcional ou seja mais abstracta e a sem ntica denotacional possuem apesar de tudo grandes similaridades Em Meyer 91 a correspond ncia matem tica mesmo estabelecida por compara o entre as defini es operacional e denotacional da mesma linguagem e pela constata o de que a vers o denotacional usa fun es de granularidade inferior s da vers o operacional por serem a vers o curried Curry et al 71 das primeiras A maior diferen a entre as abordagens consiste apenas no facto de que en quanto na abordagem operacional as constru es sint cticas s o definidas rela tivamente a um par lt entrada estado gt na abordagem denotacional apenas as constru es sint cticas s o consideradas havendo assim um maior n vel de abstrac o Finalmente note se que em ambas as abordagens um modelo da linguagem constru do sendo num caso mais operacional e de baixo n vel enquanto que no outro de cariz mais matem tico e formal Se
10. entre sintaxe e sem ntica A sem ntica define os efeitos e os resultados das diferentes constru es sint cti cas da linguagem O significado sem ntica est pois intrinsecamente ligado forma sintaxe pelo que qualquer m todo de defini o sem ntica de linguagens se baseia neste facto A defini o da sintaxe concreta de uma linguagem de programa o feita usando o standardizado formalismo designado por Backus Naur Form ou BNF empregue pela primeira vez na descri o da linguagem Algol 60 Naur 60 A de fini o matem tica da sem ntica de linguagens de programa o de tipo impera tivo foi sempre um problema encarado como relevante ainda que dadas certas caracter sticas destas linguagens o processo se tivesse revelado de grande com plexidade matem tica e portanto n o muito atractivo e pouco empregue De facto as linguagens imperativas possuem por forma a serem eficientes constru es muito ligadas arquitectura da m quina logo pouco abstractas em rela o mesma Assim instru es correspondendo a directivas s o as unida des b sicas de programa o e programas meras sequ ncias de instru es cujo objectivo actuar sobre o estado da m quina subjacente A sequencia o expl cita das instru es atrav s da utiliza o de estruturas de controlo obrigando a que a complexidade de um problema seja resolvida atrav s do seu fracciona mento segundo uma ordem temporal 3 cf a Confer ncia IFIP s
11. es no por vezes elevado conjunto de conhecimentos de matem tica e l gica que t m que ser invocados Nenhuma linguagem de base alg brica at agora surgida trata quest es temporais dado assentarem numa base funcional Problemas relacionados com a modularidade a parametriza o e o refinamento de especifica es 31 hidden operators CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 92 alg bricas t m vindo a ser abordados com sucesso em sistemas tais como ML Harper 86 ou OBJ Goguen e Meseguer 82 com implementa es dispon veis ou ainda no sistema Larch Horning et al 85 ainda em desenvolvimento O tratamento de erros e a express o de falha de comportamento s o em geral de tratamento complexo na abordagem alg brica O problema reside no facto de que quando as fun es podem ser parciais i n o definidas em pontos dos seus dom nios uma adicional e consider vel complexidade notacional tem que ser introduzida As actuais abordagens v o da pura exclus o da express o de situa es de erro inclus o de um elemento gen rico de erro indefinido ou mesmo apenas em trabalhos te ricos introdu o de valores de erro associados s esp cies Em Ehrig e Mahr 85 apresentada uma completa revis o dos conceitos al g bricos fundamentais ao m todo 3 4 2 M todos baseados em Modelos Na abordagem alg brica a cada esp cie ou tipo associado um identificador s o dadas as assinaturas
12. nesta tese se assume como o m todo utilizado para o desenvolvimento da camada computacional A linguagem de especifica o CAMILA utilizada para a apresenta o de todas as especifica es realizadas ao longo da tese merece por tal motivo especial aten o sendo lhe dedicado tamb m o AP NDICE A
13. o ao declarativo l gico Warren 77 ou funcional M cCarthy 62 CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 69 m todos e formalismos de especifica o e desenvolvimento de programas e entre eles os utilizados nesta tese 3 2 Correc o de Programas Embora a evolu o da Engenharia da Programa o tenha demonstrado que propriedades tais como a legibilidade do c digo a modularidade a reutiliza o a normaliza o a usabilidade e outras s o importantes necess rio que se fa a alguma distin o entre as propriedades que revelam qualidade no processo e aquelas que s o cruciais quanto qualidade do produto Por exemplo princ pios e propriedades tais como legibilidade do c digo estrutura o modularidade e reutiliza o t m a ver com o processo ou seja a sua aplica o pretende garantir a melhor qualidade do processo de fabrico do produto procurando uma maior facilidade das pr ticas e uma diminui o dos custos Por m as propriedades ligadas qualidade do produto s o diferentes podendo n o ter directamente a ver com a qualidade do processo ainda que a garantia de tal relacionamento seja um objectivo fundamental de estudo na disciplina ou seja procurando garantir que bons processos conduzam a bons produtos Duas das cruciais qualidades do produto software interactivo s o a sua correc o e a sua usabilidade A correc o uma propriedade fundamental porque indispen
14. o super paralelismo dentro do mesmo modelo computacional tais como em Batcher 80 Darpa 83 outras procurando CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 67 arquitecturas ajustadas a modelos computacionais alternativos como por exemplo m quinas dataflow Gurd e Treleaven 76 e m quinas de redu o Darlington e Reeve 81 e ainda os que procuraram alternativas ao n vel dos processadores como processadores do tipo RISC Patterson e Sequin 82 ou os transputers Walker 85 Como sabemos hoje em dia muitas destas tentativas acabaram por n o sobreviver ao modelo que procuravam substituir at de salientar que a maior parte destas propostas fracassa pelas mesmas raz es por que anteriormente se haviam assumido como alternativas ou seja a incapacidade do software exis tente ou desenvolvido tirar completo proveito das suas potencialidades no entanto ineg vel que a Engenharia da Programa o tem hoje em dia ao seu dispor hardware de grandes capacidades computacionais traduzido em main frames poderosos workstations sofisticadas computadores pessoais r pidos redes com razo veis velocidades de transmiss o e sistemas operativos bastante fi veis e eficientes Por m do ponto de vista do software e da Engenharia da Programa o parece ser evidente que a evolu o tem sido bastante mais lenta principalmente ao n vel dos m todos e das t cnicas Como disciplina c
15. retira primeiro first queue elem determina primeiro len queue nat comprimento da fila empty queue bool est vazia axioms q queue e elem first initq dequeue initg len initq O empty initq true first enqueue g e empty g e empty q first q empty enqueue g e false len enqueue g e 1 len q len dequeue g len q 1 end O facto de as opera es do TAD serem associadas a fun es matem ticas gera por vezes alguma incompreens o resultante na maioria dos casos de muitos anos de experi ncia e utiliza o de modelos imperativos No exemplo anterior a opera o dequeue que remove o primeiro elemento da fila por ser uma fun o matem tica n o d como resultado o elemento retirado e uma CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 89 nova queue como seria de esperar num contexto de comandos e n o de Jun es28 mas apenas a nova queue reservando se a opera o first para a determina o de qual o primeiro elemento da fila A composi o funcional poder garantir a funcionalidade de um comando por m segundo regras bem conhecidas e com significado matem tico Dentre as opera es de um dado TAD tr s distintas classes podem sempre ser reconhecidas Os construtores ou geradores que s o o conjunto m nimo de opera es necess rias para representar em abstracto i por express es ou ter mos todos os poss
16. se tiverem o mesmo tra ot ou seja a mesma sequ ncia de eventos at um certo ponto no tempo Em S no entanto equival ncia comportamental definida recorrendo no o de bissimilaridade ou de equival ncia observacional que abstrai dos eventos ou ac es invis veis e considera apenas a igualdade da sequ ncia de eventos que at um dado instante foram realizados e dos conjuntos de futuros eventos Do ponto de vista pragm tico importante afirmar que o CCS o modelo de base do formalismo de especifica o de protocolos LOTOS Bolognesi e Briskma 87 enquanto que a linguagem Occam INMOS 84 linguagem de programa o de transputers baseada no CSP De salientar ainda que esta perspectiva da estrutura o dos sistemas com base em agentes bem como a vis o dos seus comportamentos como resultantes da comunica o entre os seus agentes logo com base em controlo distribu do e concorr ncia tem sido igualmente utilizada na especifica o da estrutura e comportamento de Sistemas Interactivos em geral recorrendo a CSP para a des cri o da componente comportamental Alexander 87 Abowd 91 Uma abordagem formal aos modelos de agentes muito importante pode ser encontrada em Henessy 88 3 5 O M todo de Especifica o CAMILA SETS Apresentam se nesta sec o as ideias principais do m todo de desenvolvimento formal de sistemas software designado CAMILA SETS que apesar de continuar em desenvolviment
17. um termo da esp cie de interesse d o como resultado um outro termo dessa esp cie naturalmente alterado Note se ainda que este tipo de caracteriza o das opera es ou fun es vai ser partilhada com a abordagem por modelos ou estados expl citos onde o problema que se coloca deixa de ser a manipula o de termos da esp cie princi pal mas sim a altera o do valor corrente de um estado representado por um mo delo matem tico Poder se agora compreender que a diferen a das 27 onde efeitos laterais s o permitidos e largamente usados 28 onde n o existem efeitos laterais e apenas um resultado produzido CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 90 abordagens se situa na forma mais ou menos expl cita de representa o de tal estado ou seja termos versus valores de modelos matem ticos Do ponto de vista sem ntico a mais usual interpreta o dos axiomas a designada interpreta o equacional ainda que n o seja a nica i a que estabelece uma rela o de igualdade entre termos Estas especifica es t m por tal motivo a designa o de especifica es alg bricas equacionais Dois tipos de fecho matem tico 2 para tal conjunto de equa es s o em geral admitidos loose e initial As especifica es equacionais de tipo loose s o aquelas que fecham o sistema de equa es apenas atrav s das regras de infer ncia equa cional As especifica es do tipo
18. v rios podem ser os lugares marcados situa o que corresponde a m ltipla actividade 37 relacionadas com a possibilidade de ocorr ncia de determinados eventos 38 firing 39 enabled CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 101 Em resultado destas m ltiplas marca es situa es de conflito entre transi es podem ocorrer cf Fig 3 8 porque v rias transi es podem estar num dado momento da execu o simultaneamente habilitadas A escolha da transi o que ir ser disparada realizada de forma aleat ria dentro do modelo ou por entidades externas n o modeladas por exemplo um utilizador externo Assim uma Rede de Petri modela a actividade do sistema como a que resulta da ocorr ncia de uma sequ ncia de eventos discretos cuja ordem uma das v rias ordens poss veis permitidas pela estrutura est tica Em resultado a execu o de uma Rede de Petri assume caracter sticas de n o determinismo o Causalidade Conflito Fig 3 8 Causalidade e Conflito em Redes de Petri A vantagem de abstrac o na modela o que o n o determinismo introduz tem por desvantagem o aumento da complexidade dos tratamentos formais do modelo A restri o de que o disparo de uma transi o seja instant nea ou seja em tempo zero garante a n o simultaneidade da ocorr ncia de eventos vistos como at micos ou primitivos e portanto n o simultaneidade nos disparos das transi es Assim o mo
19. CAP TULO 3 M TODOS FORMAIS EM ENGENHARIA DA PROGRAMA O NDICE 3ks nha o 6 bi Gr 1 6 PDR SIC ES RESORT 66 3 2 Correc o de Programas suis CET DRE IR ETA 69 3 2 1 Sem ntica das Linguagens ssssssssresssesesssreserssersserereserseee 70 Sem ntica Operacional qtos pao sda nsasa lago salni andas grassa 172 Sem ntica Translacional caaesasadidisesass espe rasiididiis aguas quinta 73 Gram ticas de Atributos ssssssssesssssresseeessseessseeesseeesssees 74 Sem ntica Denotacional ssssssssseessseessseessseessseessssessseee 75 Sem ntica Axiom tica esii eo eieiei anneni reiia serrana 76 3 2 2 Verifica o de Programas O c digo iii 78 3 2 3 Tipos Abstractos de Dados eesseesesesssessesseresressereerersereerereesee 82 3 3 Metodos Formis aguas aatesiio eE A E EE aa E A EATER REAA 84 3 3 1 M todos Formais Motiva o ssssessssssesssessseseeessssseeseesssso 84 3 4 M todos Formais de Especifica o iiii erre 86 Sd l Metodos AlPCDECOS ssasieaizes dera ad dada a adiar a ia Padaria 86 3 4 2 M todos baseados em Modelos iiiice cerne 91 3 4 3 Abordagens Orientadas Concorr ncia ie 96 Redes de Petr seas S sina rata e cas aaa a oie esa tia dans 98 lgebras de Processos eerereereeeeeeerererereeerererenos 101 3 5 O M todo de Especifica o CAMILA SETS ccccecicicecereeeererenens 102 3
20. M TODOS FORMAIS EM ENG DA PROGRAMA O 79 3 2 2 Verifica o de Programas O c digo A figura 3 4 adaptada de Berg et al 82 e complementada pontualmente pelo autor apresenta uma taxonomia das mais bem conhecidas abordagens defi ni o da sem ntica das linguagens e verifica o de programas Das diferentes abordagens verifica o da correc o de programas s o de distinguir desde logo duas grandes alternativas os testes e as provas de cor rec o Porque a primeira implica a real execu o do programa designa se tam b m por verifica o din mica enquanto que a segunda por n o implicar execu o mas apenas an lise documental se designa por verifica o est tica Os testes est o directamente ligados a uma das mais antigas defini es de programa correcto em particular a que defende que um programa estar correcto desde que a sua execu o seja observacionalmente correcta i n o mostrando defeitos de execu o interna tornados evidentes pela observa o dos resultados produzidos ou n o i o seu outpu Esta perspectiva de detec o de erros estreitamente associada aos resultados observados implica de imediato que as tentativas de detec o de mau funcionamento sejam apenas aplic veis numa fase reconhecidamente muito tardia da concep o de aplica es a execu o A inefic cia do m todo directamente associ vel sua falta de rigor cient fico Dijkstra 76 8 bem c
21. a comunidade acad mica e cient fica para a resolver Nos anos 70 a crise ressurge no seu expoente m ximo em resultado da alar mante constata o de que pela primeira vez na hist ria da computa o os cus tos do software superam os custos do hardware Destas crises resultaram os principais alertas para a necessidade premente de mais rigorosamente ser compreendida e explicada a Computa o em geral bem como de capacitar a Engenharia da Programa o com ferramentas mais adequadas e produtivas e ainda de bases te ricas e m todos que cada vez mais se assemelhem em termos de produtividade rigor e fiabilidade aos que s o uti lizados nas engenharias mais tradicionais A comunidade cient fica da rea respondeu nos anos 60 e 70 com um surpreendente leque de inovadoras e multi facetadas propostas luz das quais a maioria dos desenvolvimentos actuais s o ainda realizados As propostas mais radicais assentaram na tese de que a origem de toda a obstru o ao normal desenvolvimento da Computa o residia basicamente na adop o de um modelo computacional limitado por ser sequencial o modelo de Von Neumann Backus Backus 78 ficou como um dos ex libris de tal radi calismo Assim o esfor o natural foi no sentido da procura de arquitecturas e de mo delos computacionais alternativos Com o objectivo de minorar os problemas de efici ncia arquitecturas paralelas foram desenvolvidas algumas procurando explorar
22. a sua concep o Por outro lado o m todo baseado na tecnologia subjacente suporta a cons tru o de simuladores da aplica o atrav s da liga o de uma camada interacti va entretando desenvolvida ao c digo do prot tipo da aplica o De momento s o comuns liga es do c digo do prot tipo a IU escritas quer em VisualBasic sobre Windows quer em C sobre X Windows tendo por base protocolos de co munica o CAMILA C e C CAMIA A linguagem C funciona aqui como linguagem intermedi ria A IU sempre programada independentemente do prot tipo o que se salienta nas figuras 3 9 e 3 10 separando de forma clara os dois m du los CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 105 Este simulador da aplica o poder agora ser utilizado para se iterar com o cliente quer aspectos de concep o da camada computacional quer aspectos de constru o da camada interactiva o que se torna poss vel numa fase bastante inicial do projecto com todas as bvias vantagens da resultantes IU Prot tipo Simulador da Aplica o Fig 3 10 Liga o Prot tipo Interface Ap s as necess rias itera es sobre este simulador e fixada com o cliente a funcionalidade final a implementar e at eventualmente aspectos de apresen ta o e comportamento da IU um manual de utiliza o poder de imediato pas sar a ser criado Numa situa o ideal de celebra o de contrato este simulador deveria ser at tomado como re
23. aixa de texto abaixo a teoria de um TAD Queue parametri zada pela teoria Elem que define a esp cie e opera es que podem ser feitas com tais elementos A teoria Queue parametrizada relativamente a uma qualquer teoria Elem que obede a assinatura AssElem ou seja que tenha esp cies e opera es tais como definidas em AssElem e importa conforme a cl usula uses as teorias dos naturais Nat e dos booleanos Boolean As esp cies 25 ver defini es no Ap ndice B 26 sorts CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 88 importa das cf nat importada de Nat e bool importada de Bool designam se esp cies primitivas Nas esp cies n o primitivas vulgar identificar uma esp cie designa da como principal que aquela que representa os objectos mais relevantes que o tipo exporta cf queue no exemplo em curso Broy et al 84 A sem ntica de cada uma das opera es representadas como fun es defi nidas para uma queue neste caso dada pelo conjunto de axiomas da teoria que definem rela es entre elas interpretadas como sendo propriedades relativas ao seu comportamento observ vel Da que muitas vezes se designem os m todos alg bricos como m todos orientados s propriedades ADT Queue Elem AssElem uses Nat Boolean sorts queue elem from Elem nat from Nat bool from Boolean opers initg queue inicializa o enqueue queue x elem queue inser o dequeue queue queue
24. al baseada em transi es de estados de tipo atemporal e in terior oferecida pelos TAD A modela o completa de um sistema concorrente composto por agentes ou processos sequenciais comunicantes envolver a especifica o a determinado n vel de abstrac o de quatro componentes principais o comportamento interno de cada agente o seu comportamento externo a estrutura o do sistema em agentes e a comunica o entre estes O especifica o do comportamento interno de um agente processo consiste da especifica o da estrutura do seu estado interno e privado em termos de um conjunto de atributos do conjunto de opera es de acesso a tal estado do conjunto de estados internos v lidos do poss vel conjunto de estados iniciais e das poss veis transi es de estado associadas a cada opera o definida Dado o conjunto de estados iniciais e o conjunto das opera es a especifica o interna tem impl cita um conjunto de sequ ncias poss veis de transi es de estado Por exemplo nas anteriores especifica es de uma Queue n o existe nenhuma ope ra o que permita transitar de uma queue CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 99 com dez elementos para uma queue vazia Tal pode ser inferido das opera es disponibilizadas Por outro lado foi igualmente especificado que encontrando se uma queue vazia qualquer tenta tiva de realizar o dequeue de um elemento n o ser uma transi o aceit vel No e
25. alizados por Kowalski Kowalski 74 e ML Harper 86 todas pretendendo realmente abstrair da arquitectura real e ser um passo em frente relativamente ao tratamento sem ntico formal dos programas para que se possam estabelecer racioc nios matem ticos sobre a sua fun o de execu o e n o apenas quanto sua mais ou menos eficiente compila o A tabela 3 1 sintetiza as abordagens actualmente melhor referenciadas para a defini o da sem ntica das linguagens de programa o LP Estes m todos ou classes de m todos s o de seguida apresentados de forma resumida A im port ncia da sua refer ncia resulta de muitos deles estarem na base dos m to dos de verifica o da correc o de programas que ser o introduzidos na sec o seguinte e ainda porque alguns deles ou seus derivados s o nesta tese empre gues ou referidos Operacional M todos de Defini o Translacional da Sem ntica das Gram ticas Atributivas LP Denotacional A oratico Tab 3 1 Sem ntica das Linguagens 5 Esta propriedade expressa se matematicamente pela no o de substitutividade de iguais por iguais 6 side effects CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 73 Sem ntica Operacional Segundo a abordagem operacional a defini o da sem ntica de uma linguagem de programa o pode ser realizada com base numa m quina abstracta e num aut mato de interpreta o Estabelecida a m quina abstracta a sem ntica de ca
26. ca o com a excep o da abordagem axiom tica no seio da qual os mais importantes trabalhos na rea da correc o total e parcial de programas sequenciais e con correntes foram realizados No entanto a maioria destes m todos de verifica o de correc o s o voca cionados apenas para a chamada verifica o a posteriori ou seja para a realiza o de provas de correc o apenas a jusante do pr prio processo de desenvolvi mento do programa pelo que n o fomentam uma rela o estreita entre desen volvimento e correc o Em suma n o s o m todos construtivos Os m todos construtivos s o do ponto de vista do autor fundamentais para qualquer m todo rigoroso de desenvolvimento atendendo seguinte ordem de raz es A n o ser que preocupa es de correc o especifica o e prova fa am parte do pr prio processo de desenvolvimento e a sejam realizadas em pequenas unidades compon veis muito pouco prov vel que qualquer outro m todo possa alguma vez ser utilizado Poder se ia at dizer em sentido figurativo que o triplo especifica o c digo prova necessita de apoio modular As provas necessitam de ser realizadas sobre especifica es pelo que tamb m o desenvolvimento do c digo realizado tendo por referencial a especifica o e por objectivo o resultado verdadeiro para a prova o que induz igualmente m todo Os m todos construtivos Dijkstra 76 fornecem as v rias condi es b si
27. cas para que um m todo possa servir ao desenvolvimento rigoroso de programas em particular A possibilidade de se considerar uma especifica o E como sendo compon vel numa estrat gia bottom up ou decompon vel numa estra t gia top down em sub especifica es E segundo o esquema E Es Ep CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 82 emque um operador matem tico bem definido A possibilidade de se considerar um programa P como sendo compon vel numa estrat gia bottomup ou decompon vel numa estrat gia top down em sub programas P segundo o esquema P P Ph onde um construtor sint ctico da linguagem de programa o em uso A possibilidade de se considerarem pequenas provas de correc o rela cionando uma parte do programa P com uma sub especifica o E segundo o esquema P sat E A possibilidade de se combinarem as pequenas provas de correc o na prova global de correc o do programa segundo o esquema P sat E Pa sat Ep 22 P Pph sat E Ep Apesar das muitas dificuldades ainda encontradas na utiliza o trivial de m todos de desenvolvimento de programas baseados na abordagem construtiva esta perspectiva de desenvolvimento rigoroso de software constitui ainda a ba se da maior parte dos m todos formais de especifica o e desenvolvimento de programas apresentados a seguir No entanto u
28. da constru o da linguagem corresponde forma como esta executada em tal m quina sendo tal correspond ncia definida pelo interpretador abstracto o aut mato Quando rotinas de uma linguagem de programa o concreta s o usadas na escrita de tal interpretador estamos perante uma sem ntica operacional definida como concreta Quando em contrapartida s o usados objectos matem ticos em particular por exemplo usando uma nota o funcional execut vel como em Martins et al 85 estamos perante uma sem ntica operacional matem tica Em qualquer dos casos a abordagem operacional assume uma base inter pretativa contrariamente abordagem translacional que se apresentar mais frente tal como ilustrado na figura 3 1 Sem ntica Operacional Interpretador Abstracto Resultados Fig 3 1 Sem ntica Operacional de real ar ainda a semelhan a entre esta abordagem para a descri o da sem ntica de linguagens e as t cnicas de prototipagem r pida e de anima o de especifica es usadas em Engenharia da Programa o A abordagem operacional tem a sua g nese no IBM Vienna Laboratory aquando da defini o da linguagem PL I usando a linguagem VDL Wegner 72 De salientar que o m todo de especifica o e desenvolvimento de programas designado por VDM Jones 80 que ser apresentado adiante ainda que tenha sido desenvolvido a partir de VDL de base denotacional e n o operacional Sem n
29. das sob a forma gen rica Se os valores iniciais das vari veis de um programa satisfazem a rela o R1 ent o ap s termina o do programa tais valores dever o satisfazer a rela o R2 Hoare por seu lado introduz explicitamente triplos da forma P S R onde S representa uma instru o da linguagem P um predicado sobre os va lores que certas vari veis assumem antes da execu o de S a pr condi o e R um predicado sobre os valores que tais vari veis devem assumir ap s a execu o de S a p s condi o com a seguinte interpreta o Admitindo que P verdadeiro antes da execu o de S e admitindo que S termina ent o R verdadeiro ap s a execu o de S Ainda que n o constituam uma inova o relativamente s asser es de Floyd os triplos de Hoare apresentam no entanto a si associadas regras formais de manipula o e as bases de uma metodologia para desenvolvimento formal de programas Hoare apresenta regras de c lculo de consequentes permitindo determinar de forma l gica pr condi es mais fortes e p s condi es mais fracas Estas f rmulas s o conhecidas por axiomas de Hoare De import ncia crucial o facto de o m todo proposto por Hoare ser contra riamente ao de Floyd composicional i definidas as propriedades das instru es simples as propriedades de uma qualquer instru o composta podem ser deduzidas a partir das suas componentes 4 Por exem
30. delo para al m de n o determinista implica n o simultaneida de Eventos n o at micos ou seja n o instant neos podem ser estruturados em sequ ncias de eventos at micos Considerando que a rede total composta pelas diversas partes do sistema a modelar a natureza ass ncrona das Redes de Petri torna se clara quando se verifica que os eventos que dizem respeito a cada componente ocorrem em completa independ ncia uns dos outros Adicionalmente a sincroniza o de actividades tamb m de f cil express o sendo criados lugares que estabelecem a liga o s ncrona de comportamentos Formalmente uma Rede de Petri R numa das suas formas mais simples pode ser definida como sendo o tuplo R lt P T F M gt sendo respectivamente P um conjunto de estados locais marcados ou n o ou condi es T um conjunto de transi es F um par formado pelas fun es de incid ncia F e F representando respectivamente os arcos de entrada e CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 102 de sa da de cada transi o e M a fun o de distribui o que associa a cada lugar o n mero de tokens nele contidos Por raz es que se prendem com necessidades espec ficas de adequa o das Redes de Petri modela o de problemas com caracter sticas particulares s o muitas as extens es a este modelo base que t m vindo a ser desenvolvidas Por exemplo cf Reisig 85 Higher Level Petri Nets procurando resolver proble
31. e ricos apresentam se ainda assim as principais abordagens especifica o de sistemas concorrentes ou se se pretender de sistemas de processos ou agentes Duas grandes classes de m to dos s o aqui considerados Redes de Petri e lgebras de Processos Redes de Petri Redes de Petr s o modelos abstractos e formais que representam o fluxo e o controlo de informa o num sistema A teoria das Redes de Petri devida a Carl Petri que na sua tese de doutoramento Petri 62 desenvolveu um modelo do fluxo de informa o em sistemas exibindo concorr ncia ass ncrona S o refer nci as obrigat rias sobre este tipo de formalismo os trabalhos de Peterson Peterson 77 e de Reisig Reisig 85 As Redes de Petri t m sido usadas com especial incid ncia na especifica o do comportamento de sistemas reactivos ou seja sistemas que 35 veja se o que se passa igualmente na rea da simula o de sistemas 36 Petri Nets CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 100 s o tipicamente event driven por acomodarem com facilidade e at naturalidade as no es de evento e estado A no o de transi o de estado associada ocorr ncia de um evento expl cita neste modelo especificando se por cada ocorr ncia de evento o conjunto de estados por esta influenciados Redes de Petri assumem assim um car cter operacional dado que especificam o sistema pretendido fornecendo um modelo que simula o comportament
32. e ser garantida pela tratabilidade matem tica do formalismo empregue Entre o o qu e o como igualmente im portante que se possa considerar o porqu rigoroso ou 24 em geral consubstanciadas na frase Os m todos formais s o bons mas s o demasiado onerosos CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 86 seja a justifica o mate m tica dos passos entre as duas etapas anteriores cf a figura 3 5 refinamento prova PORQU E Fig 3 5 O M todo Rigoroso Holt em Holt 86 considera que a especifica o formal de programas a t cnica dos tr s Cs clareza coer ncia e completude Adicionalmente e ainda segundo Holt a especifica o formal de programas uma idealiza o mas enquanto tal importante pois encoraja cuidadosos e proficientes racioc nios mesmo que os passos matem ticos dos m todos n o sejam completamente cum pridos Estas considera es s o muito interessantes pois condizem com a perspec tiva pessoal do autor sobre a forma de aplica o concreta destes m todos anga riada com base em experi ncia concreta ao longo dos anos Se adicionalmente os formalismos empregues forem execut veis ent o poderemos ter modelos execut veis i prot tipos dos sistemas desde as fases mais preliminares do desenvolvimento permitindo que desde as fases iniciais as concep es possam ser operacionalmente testadas e iteradas Nestes casos para al m do rigor matem tico das de
33. ema Queue __ _ _ queue seq N vari veis queue lt 200 predicados no qual se declara a vari vel queue como sendo uma sequ ncia de naturais e no qual na metade inferior se descreve num predicado as propriedades a que os valores deste tipo devem obedecer Este esquema um definidor do tipo Queue O esquema seguinte mostra como se especifica uma opera o que receben do um argumento de entrada e vai alterar o estado da queue cf Queue e como se especifica na p s condi o o novo estado da queue representado pelo identificador queue E enqueue lr SL ESSAS Exa Queue e N Para al m deste tipo de especifica es baseadas em pr e p s condi es tal como em VDM Z permite tamb m especifica es puramente funcionais e at especifica es nica e simplesmente baseadas em predicados e portanto mais orientadas s propriedades A linguagem de esquemas permite a comunica o entre esquemas sob a forma de passagem de determinados dados quer de modo sequencial quer sob um mecanismo de piping sendo no entanto esta comunica o de um para um 34 scheme CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 98 A possibilidade de especifica o modular existente em Z no entanto desacompanhada da exist ncia de um m todo ou pelo menos de alguma nor maliza o na sua aplica o pelo que em geral as apresenta es acabam por ser realizadas com estilos muito dif
34. ente observ vel Em ambas as perspectivas uma vis o se quencial ou concorrente de tais comportamentos pode ser tomada ainda que tal influa no formalismo a empregar em cada caso Distinguem se em geral em termos de abordagem seis grandes classes de m todos que a seguir se descrevem quanto s suas propriedades e capacidades Para que um contexto comparativo possa ser estabelecido estas classes de m todos s o apresentadas e analisadas quanto sua capacidade de express o de funcionalidade tempo e erros ou falhas quanto forma como permitem ou n o refinamento e ainda quanto ao factor subjectivo da sua clareza 3 4 1 M todos Alg bricos Os m todos alg bricos est o em estreita liga o com a no o de tipo abstracto de dados e com a necessidade de se realizar uma caracteriza o matem tica destes de forma completamente abstracta ou seja definindo um conjunto de propriedades a respeitar pelas suas opera es e sem fazer qualquer refer ncia ao estado interno Formalmente cada tipo abstracto de dados neste m todo uma unidade b sica de especifica o sendo estas especifica es vistas como teorias28 ou seja como pares de assinaturas e axiomas Assinaturas definem a componente sint ctica do TAD ou seja os tipos nele envolvidos em rigor esp cies e a funcionalidade dos operadores Axiomas definem num dado contexto l gico de interpreta o rela es entre opera es Especifica se na c
35. erentes e nem sempre leg veis necessitando por vezes da introdu o de algumas extens es visando a sua utiliza o em grandes especifica es Martins 87a Os maiores projectos envolvendo especifica es realizadas na linguagem Z foram aparentemente a especifica o do sistema transaccional CICS da IBM enquanto que VDM foi aplicado para al m da especifica o das linguagens re feridas na especifica o da base de dados relacional System R igualmente para a IBM Em Monahan e Shaw 91 apresentada uma interessante perspectiva hist rica destes m todos VDM e Z bem como uma compara o das suas g neses e das suas actuais diferen as t cnicas 3 4 3 Abordagens Orientadas Concorr ncia Incluir se o nesta sec o refer ncias s principais abordagens dispon veis especifica o de sistemas exibindo paralelismo concorr ncia e comunica o nos seus componentes ou seja sistemas nos quais existem entidades aut nomas interac o entre estas entidades a qualquer momento das suas execu es tendo o sistema que gerir comunica o sobreposta no tempo simult nea entre os seus componentes Em geral estas entidades s o formalizadas como agentes ou processos in ternamente sequenciais e comunicantes associados a uma componente de comportamento din mico resultante da sua interac o por comunica o numa escala temporal que mais abstracta ou mais concreta incompat vel com a vis o mais funcion
36. esmo foi constru do Assim a adop o de m todos formais uma decis o de projecto e de processo de interesse apenas directamente mensur vel pelas equipas de concep o e desenvolvimento de programas Embora possamos ser ainda hoje confrontados com algumas resist ncias sua aplica o em geral por discut veis raz es de ndole pragm tica2 a realidade vem demonstrando uma crescente ader ncia nas mais diversas reas a estes m todos rigorosos de concep o e desenvolvimento de projectos Como se procurou salientar na sec o anterior a quest o fundamental a introdu o de rigor no processo A descri o formal de um sistema consiste na express o rigorosa de base matem tica de determinadas caracter sticas fundamentais dos sistemas soft ware Podemos descrever formalmente as suas caracter sticas estruturais de funcionalidade de comportamento interno ou de comportamento externo ou seja de interac o com outros sistemas A utiliza o de formalismos ou nota es rigorosas que garantam n o ambiguidade abstrac o e at possibilidade de racioc nio sobre determinadas propriedades uma condi o indispens vel A n o ambiguidade garante interpreta o nica A abstrac o garante elimi na o de detalhe e concentra o sobre o que o sistema deve fazer e afastamen to ainda que tempor rio relativamente a como o deve fazer A possibilidade de racioc nio sobre propriedades do sistema dev
37. eue queue retira primeiro dequeue g pre cond empty g tail g first queue elem determina primeiro pre cond empty q head g 32 correspond ncias CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 94 len queue nat comprimento da fila len g length g empty queue bool est vazia empty g q lt gt Foi propositadamente introduzido um predicado sobre os valores do tipo do estado Queue indicando que nenhuma queue v lida poder conter mais de 199 elementos Este predicado que determina a gama de valores v lidos e inv lidos do estado designa se invariante de tipo de dados e deve ser satisfeito por todas as opera es que alteram o estado sendo bvio que a opera o cr tica a ope ra o de modifica o do estado enqueue Algumas das fun es possuem uma cl usula designada pr condi o que indica que a fun o n o uma fun o total ou seja definida para todos os valores do seu dom nio argumentos indicando se explicitamente em que casos o resultado da fun o n o se encontra definido No exemplo torna se claro que as fun es dequeue e first s o indefinidas caso a queue par metro se encontre vazia note se a rela o com os axiomas de erro da especifica o alg brica S o estes os principais componentes de uma especifica o baseada em modelos Dependendo dos formalismos empregues ap s a constru o deste modelo alguns
38. ferencial para a celebra o do mesmo devendo o sistema final ser com este confrontado em situa es de d vida quanto satisfa o dos requisitos do projecto Este procedimento poderia trazer Engenharia da Programa o uma credibilidade acrescida e a ambas as partes contratantes e contratados um maior grau de seguran a e comprometimento Estabelecido deste modo ideal ou n o o contrato o desenvolvimento do sis tema prosseguir de seguida no sentido da constru o de c digo eficiente para a camada computacional Partindo da especifica o formal constru da a imple menta o final calculada com base em regras definidas no c lculo de SETS formalizado e apresentado em Oliveira 92 Como este refinamento pode e deve ser realizado de forma gradual poder o existir fases no projecto em que c digo final coexista com c digo do prot tipo mantendo se assim sempre dispon vel a funcionalidade global inicialmente prometida CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 106 Prot tipo Fig 3 11 Implementa o Gradual Finalmente o c digo da IU anteriormente fixado ligado implementa o final da camada computacional assim se criando o Sistema Interactivo Em s ntese o m todo CAMILA SETS fornece para al m do rigor que pode ser encontrado em m todos baseados em modelos matem ticos como VDM e Z an teriormente apresentados vantagens adicionais de utiliza o designadamente Pos
39. icado P satisfaz sua especifica o E igualmente estabelecida de modo rigoroso Ou seja trata se de calcular a express o de prova seguinte es crita seguindo a nota o apresentada em Oliveira 94 IP sat E Como j se referiu apenas possuindo uma defini o rigorosa da sem ntica da linguagem de programa o se torna poss vel obter o significado de P Por outro lado s possuindo uma especifica o E igualmente de significado rigoroso e matem tico a prova de satisfa o pode ser realizada O tipo de suporte matem tico empregue em cada uma das abordagens para a defini o da sem ntica das linguagens de programa o e portanto dos pro gramas vai decididamente influenciar a defini o de P a formula o de E e o mecanismo de prova de sat CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 81 Por verifica o da correc o de um programa neste contexto formal deve pois entender se a prova est tica e matem tica de que um programa P cujo sig nificado matem tico se denota por P e para o qual se formulou uma especifica o precisa E cumpre as condi es de correc o designadamente finito isto termina satisfaz a sua especifica o ou seja P sat E sendo sata rela o l gica de satisfa o expressa no formalismo adequado A figura 3 4 mostra claramente que a maioria das abordagens para a verifica o sem ntica das linguagens n o teve continua o na rea da verifi
40. ient fica a Ci ncia da Computa o surge nos anos 60 com o objectivo de desenvolver as bases te ricas que permitam fornecer explica es rigorosas e tratamento matem tico para os mais diversos processos computacio nais Teorias como a das Fun es Recursivas dos Grafos dos Aut matos a l gebra e a L gica s o muitos dos exemplos de conhecimentos matem ticos que passaram a ser usados em Ci ncia da Computa o A Ci ncia da Computa o moderna tal como a conhecemos actualmente tem aqui a sua g nese preocupada em possuir uma base te rica e formal mas suficientemente pragm tica para se assumir como uma ci ncia aplicada reso lu o dos problemas na rea da computa o Esta filosofia sintetizada por Knuth em Knuth 71 quando afirma A minha experi ncia a de que teorias s o muitas vezes mais estruturadas e mais interessantes quando s o baseadas em problemas reais de alguma maneira elas s o mais excitantes do que algumas vez poder o ser as teorias completamente abstractas A Engenharia da Programa o encontra na Ci ncia da Computa o a sua ci ncia de suporte A Ci ncia da Computa o tem disponibilizado Engenharia da Programa o para al m das evolu es e resultados pr prios desta enquanto disciplina de engenharia resultados de grande valor cient fico O objectivo conforme o ciclo de evolu o tecnol gica de CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 68 Marche
41. inda que sint tica da evolu o das Ci ncias da Computa o em particular no sentido de prover a Engenharia da Programa o com o rigor indispens vel credibilidade do projecto de software As principais contribui es para a defini o da sem ntica de linguagens de pro grama o foram apresentadas Tendo as linguagens uma sem ntica precisa a verifica o da correc o de programas passa a ser poss vel e as principais abor dagens com tal objectivo foram referidas tendo se salientado a import ncia das abordagens construtivas Foi apresentado o conceito de Tipo Abstracto de Dados TAD possivelmente uma das no es mais importantes em Ci ncias da Compu ta o das ltimas d cadas com reflexos relevantes quer na pr tica quer nas ferramentas de Engenharia da Programa o designadamente a programa o modular e a programa o orientada aos objectos constituindo a base formal do aparecimento de diversos m todos de especifica o de sistemas A import ncia da utiliza o de m todos formais de especifica o e desenvol vimento de aplica es foi salientada tendo se ainda apresentado as mais rele vantes classes destes m todos e seus exemplares Esta apresenta o tornava se obrigat ria dado que alguns destes m todos ou seus exemplares particulares s o extensivamente aplicados ou explicitamente referidos ao longo da tese Pela mesma raz o na sec o 3 5 apresentou se o m todo CAMILA SEIS m todo que
42. initial usam para al m destas regras de in du o estrutural e a regra que determina que se uma igualdade n o pode ser deriv vel das regras de infer ncia equacional e das regras de indu o estrutural ent o a mesma corresponde a uma desigualdade ou seja advogando que partida todos os termos s o diferentes Axiomas podem assim ser vistos como equa es e regras de reescrita com os quais n o s se descreve o comportamento dos operadores sobre os objectos especificados pelos termos que em tal teoria podem ser constru dos como tam b m poss veis equival ncias na verdade congru ncias entre termos Axiomas podem tamb m especificar termos que representam comportamento de erro Por exemplo o primeiro axioma da teoria apresentada i first initg 2 especifica em abstracto um comportamento inv lido que o que resulta de se tentar determinar qual o primeiro elemento de uma fila de espera que acabou de ser inicializada criada e que logicamente est vazia O axioma determina como indefinido indefin vel ou erro o resultado de tal sucess o de opera es30 Em geral a sem ntica completa de uma opera o s pode ser compreendida analisando todos os axiomas em que a mesma aparece Por exemplo relativa mente opera o de inicializa o de uma fila de espera que acima se consi derou criar uma fila de espera vazia tal sem ntica apenas garantida pela considera o dos seguintes axiomas
43. is atributivas adicionam mera descri o sint ctica de uma linguagem baseada numa gram tica conforme o atr s referido elementos que visam a descri o da sem ntica das respectivas constru es sint cticas As gram ticas de atributos foram introduzidas por Knuth em Knuth 68 tendo por ideia base um processo designado por decora o Assim quer a sinta xe de partida seja concreta ou abstracta a ideia decorar as constru es sin t cticas com atributos que descrevem as propriedades sem nticas dos elementos de tais constru es Quanto s produ es da gram tica estas s o decoradas com regras que exprimem rela es entre os CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 75 atributos das constru es do lado esquerdo da produ o com os atributos das constru es db lado direito da mes ma A sem ntica de qualquer entidade sint ctica pode assim ser em qualquer contexto vista como o resultado do c lculo dos seus atributos associados Duas formas distintas s o em geral apontadas como vias para a descri o dos atributos Uma mais procedimental ou orientada s rotinas na qual a nfase colocada nas regras outra mais orientada aos objectos onde a nfase colocada nas constru es sint cticas e seus atributos sugerindo portanto um maior grau de modularidade N o possuindo uma reconhecida liga o aos m todos de verifica o e de especifica o de programas mas antes a interessantes desen
44. k ages enquanto imperativas ML Hope e Miranda abstract type enquanto fun cionais e class em toda a fam lia de linguagens de objectos tais como ABCL 1 Smalltalk Eiffel C ou Objective C A abstrac o comum a todas estas abordagens implementa o de meca nismos de abstrac o de dados mais ou menos conseguidas22 no entanto o conceito formal de tipo abstracto de dados 23 TAD introduzido num contex to alg brico por Zilles Zilles 74 pelo grupo ADJ Goguen et al 78 e por Guttag e Horning Guttag e Horning 78 Um tipo abstracto de dados uma caracteriza o abstracta definicional das propriedades de um determinado tipo de dados sendo tal caracteriza o abstracta no sentido de que independente i afastada da efectiva imple menta o do tipo de dados Em geral um novo tipo de dados pode ser especificado com base num tipo abstracto de dados podendo ser este definido algebricamente ou usando modelos matem ticos Estas duas possibilidades encontradas ir o de facto conduzir s duas mais proeminentes abordagens especifica o de programas designadamente a abordagem alg brico funcional e a abordagem por modelos ou construtiva A possibilidade de se usarem ambas as abordagens procurando facilitar a implementa o de TAD usando prototipagem e os cuidados a ter na sua imple menta o modular usando tipos opacos em m dulos Modula 2 apresentada em
45. m ntica Axiom tica O m todo axiom tico de defini o de linguagens de programa o tem a sua g nese nos trabalhos de Floyd 67 e Hoare 69 O m todo axiom tico ao con tr rio dos at aqui apresentados n o procura estabelecer qualquer modelo para a linguagem por associa o de sem ntica a cada constru o da linguagem an tes fornecendo um c lculo com regras de deriva o e axiomas com base no qual poss vel raciocinar sobre propriedades dos programas estabelecidas usando predicados sobre os valores das respectivas vari veis Em rigor por m o m todo n o fornece directamente uma sem ntica para a linguagem n o sendo pois um m todo de descri o sem ntica No entanto o requisito de que a sem ntica da linguagem satisfa a as regras de deriva o e os axiomas do c lculo torna essa sem ntica num modelo e assim o c lculo numa descri o exacta da linguagem O pr prio Hoare afirma no seu artigo CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O qq original que os axiomas e as regras de infer ncia ou deriva o constituem a definitiva especifica o da sem ntica da linguagem Floyd em Floyd 67 usa diagramas de fluxo de controlo 3 que decora com f rmulas do c lculo de predicados de 1 ordem asser es relacionando valo res de vari veis entre si Floyd sintetiza o problema da verifica o da correc o de programas como sendo um problema de prova rigorosa de propriedades enuncia
46. m todos permitem a imediata ou quase imediata constru o de um prot tipo execut vel do sistema em desenvolvimento permitindo deste modo que numa fase muito pr via de concep o esta possa ser iterada perante um modelo ou simulador do sistema sem que seja perdida a possibilidade de tal como noutros se possam realizar provas est ticas de correc o A linguagem de especifica o CAMILA Almeida e Barbosa 91 formalismo de especifica o por modelos usado nesta tese de base funcional e possibilita o desenvolvimento r pido de prot tipos dos sistemas especificados Dada a sua import ncia pela extens o da sua utiliza o na apresenta o da tese dedica se o AP NDICE A a uma mais completa apresenta o das suas caracter sticas e da sua sintaxe Terminada a fase de constru o e possivelmente itera o de uma especifica o formal segue se a fase em que a partir desta uma implementa o deve ser constru da Os passos necess rios passagem deste n vel abstracto at ao n vel concreto de uma implementa o por refinamento ou transforma o n o s o em geral contemplados de forma sistem tica Excep o deve ser feita ao Vienna Development Method VDM Jones 80 Jones 90 que pela sua maturidade e pelo pragm tico compromisso entre CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 95 rigor e total formalidade sugere um m todo eficaz para se atingirem implementa es correctas a partir de es
47. ma complementar e inovadora perspectiva de desenvolvimento rigoroso de programas a partir de especifica es vem sendo proposta baseada na ideia de que com base num c lculo dedutivo a estabelecer de facto regras de deriva o poder ser poss vel calcular classes de programas satisfazendo s especifica es dadas Oliveira 92 cuja aplicabilidade pr tica e vantagens se procurou salientar num contexto de desenvolvimento em Martins 88a Esta abordagem de alguma forma uma vers o actualizada das ideias defendidas pela abordagem iniciada por Burstall e Darlington Burstall e Darlington 77 designada por abordagem transformacional A ideia fundamental consiste em definir um c lculo de base matem tica que garanta que partindo de uma especifica o por transforma es sucessivas seguindo as regras do c lculo se obt m o c digo final correcto Sendo o c lculo semanticamente rigoroso a correc o estar automaticamente garantida sendo as provas de correc o dispensadas dada a correc o impl cita do c lculo Este c lculo de programas designado por SETS Oliveira 90 92 serve de base a um esquema de refinamento de CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 83 especifica es em programas que se designou por refinamento transformacional ou c lculo de programas Morgan e Gardiner 90 O pr prio c lculo de Oxford Morgan e Gardiner 90 pode ser visto como uma no va ordem de ideias para o c lc
48. mas de estrutura o Stochastic e Timed Petri Nets procurando incorporar restri es temporais no modelo e Predicate Transition Nets que incorporam vari veis e pre dicados que s o escritos sobre estas e v o condicionar transi es As caracter sticas operacionais das Redes de Petri bem como a sua s lida e extensa base te rica aliadas exist ncia de uma representa o diagram tica fazem das Redes de Petri um dos formalismos de modela o de sistemas concorrentes mais empregues em contextos industriais In meras ferramentas gr ficas t m vindo a ser desenvolvidas para que a sua constru o seja feita de forma interactiva e validada bem como outras para a an lise e verifica o de diversas propriedades din micas dos sistemas modelados As Redes de Petri s o tamb m bastante adequadas prototipagem r pida de sistemas pela operacionaliza o do modelo que representam dada a facilidade de interpreta o e de execu o da representa o deste As Redes de Petri ser o nesta tese utilizadas para a defini o da sem ntica operacional dos Gui es de Interac o o formalismo de especifica o de di logos que ir ser apresentado na sec o 6 2 Definida a sua sem ntica operacional deste modo as Redes de Petri resultantes da tradu o dos Gui es de Interac o constituir o a base para a gera o de prot tipos dos controladores do di logo assim especificados lgebras de Processos lgebras de Processos
49. mo wp S R e ao su gerir regras para tal c lculo que designou por transformadores de predicados Por exemplo para o caso da sequencia o acima referido a regra seguinte poderia ser considerada wp S1 S2 R wp S1 wp S2 R A perspectiva de Dijkstra bastante diferente da anterior dado que prop e que todas as constru es dos programas sejam vistas como transformadores de p s condi es requisitos nas mais fracas pr condi es que as garantam Es ta perspectiva vai de encontro a preocupa es de aplicabilidade destes m todos formais na concep o e no desenvolvimento de programas at a pouco conside rada ou impratic vel assim que a programa o estruturada sugerida por Dijkstra em Dijkstra 76 ao contr rio do que muitas vezes se refere n o um mero marco estil stico mas antes um passo no sentido da aplicabilidade destes m todos a programas imperativos por elimina o das constru es destes que s o matematicamente intrat veis O m todo de Dijkstra tamb m mais completo pois permite provar a correc o total Como veremos na sec o seguinte onde se aborda o problema mais espec fico da verifica o de programas o m todo axiom tico em particular a partir dos trabalhos referidos conduziu a enormes avan os na rea da verifica o da correc o de programas quer sequenciais quer concorrentes 15 strongest verifiable consequent 16 weakest precondition CAP TULO 3
50. ns s o supostos possuir uma sem ntica assente em objectos matem ticos bem conhecidos com propriedades alg bricas e l gicas que permitem o seu tratamento matem tico visando a prova matem tica da sua correc o Estas linguagens surgem assim n o tanto com o objectivo cl ssico de garantirem efici ncia na sua compila o mas antes procurando que ao ser lhes associada uma sem ntica matem tica tal possa tornar mais f cil o tratamento matem tico dos seus programas e portanto a pr pria verifica o da sua correc o por meio de prova matem tica neste tipo de preocupa es que se pode encontrar a g nese do apareci mento dos M todos Formais de descri o e especifica o de programas e siste mas ocorrida no in cio dos anos 80 A verifica o da correc o para al m de idealmente dever ser realizada num contexto matem tico deve ter em conside ra o os pr prios requisitos funcionais entre outros estabelecidos para o pro grama Passa ent o a ser tamb m fundamental que tais requisitos sejam igualmente captados formalmente ou seja sejam eles pr prios matematicamen te represent veis e trat veis Esta liga o entre verifica o formal e especifica o de requisitos ou seja entre m todos de verifica o e m todos de especifica o justifica que na sec o seguinte se abordem os primeiros tanto mais que foram os percussores dos segundos apresentando se na sec o 3 3 os principais 1 por oposi
51. ntanto a express o destas restri es s transi es de estados ou seja sequ ncia de opera es n o realizada explicitamente sendo em geral dif cil de ser feita em termos de transi es de estados Assim uma alternativa consiste em considerar se que estas opera es v o ser executadas em resultado da recep o de eventos resultantes da interac o do agente com outros agentes e assim restri es de comportamento passam a ser descritas como restri es sobre a sequ ncia de eventos aceit veis pelo agente A especifica o deste com portamento sob a forma de predicados sobre os eventos em que o agente pode participar designa se por especifica o do comportamento externo ou seja externamente observ vel A comunica o o mecanismo atrav s do qual eventos s o transmitidos entre agentes A discretiza o da dimens o cont nua temporal na an lise e representa o do comportamento de sistemas concorrentes como mecanismo de abstrac o faz com que a unidade at mica em geral indivis vel a considerar como base de evolu o passe a ser o evento Assim de salientar que o comportamento global observ vel de um sistema concorrente vai depender dos comportamentos indi viduais dos seus componentes por sua vez dependentes das suas transi es internas de estados por seu lado fun o do modo como o sistema lida com a potencial simultaneidade da ocorr ncia de eventos Mesmo que n o entrando em detalhes t
52. o actualmente leccionado e empregue no Departamento de Inform tica da Universidade do Minho A figura 3 9 procura ilustrar o Ciclo de Vida do Software tal como proposto pelo m todo Considerados os requisitos gerais do sistema a construir uma es pecifica o formal em CAMILA SETS desenvolvida Esta especifica o pode ser a um primeiro n vel realizada sob a forma de uma especifica o alg brica equa cional ou teoria alg brica do problema Esta especifica o dado o 40 do ingl s trace CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 104 seu elevado n vel de abstrac o poder servir para que propriedades dos sistemas possam ser em abstracto provadas num contexto alg brico itera o com contratante equipa reutiliza o E Manual de gil Utiliza o Biblioteca de Componentes Reutiliz veis Manuten o Fig 3 9 O M todo de Desenvolvimento CAMILA SETS O passo seguinte consiste no desenvolvimento possivelmente modular de um modelo matem tico dessa teoria alg brica recorrendo linguagem CAMILA Tal modelo pode ser total ou parcialmente escrito recorrendo a uma biblioteca de componentes de especifica o reutiliz veis dispon veis em cat logo Oliveira 91 Esta constru o de um modelo abre caminho gera o autom tica de um prot tipo da camada computacional que pode de imediato ser executado e servir para a pr pria equipa de projecto iterar
53. o desejado deste A representa o pict rica de uma Rede de Petri consiste num grafo onde dois tipos de nodos podem ser reconhecidos cf Fig 3 7 c rculos designados lugares e barras designadas transi es Arcos orientados relacionam lugares com transi es e transi es com lugares Os lugares s o feitos corresponder a estados locais ou condi es3 correspondendo as transi es ocorr ncia de eventos Estas componentes desta forma relacionadas entre si representam as propriedades est ticas dos sistemas Por m as Redes de Petri representam tamb m as propriedades din micas destes atrav s do posicionamento e desloca o ao longo do grafo de marcas designadas tokens apresentadas como pontos negros que representam as con di es ou estado actual do sistema Lugar Transi o Fig 3 7 Esquemas b sicos de uma Rede de Petri A distribui o dos tokens na rede designa se por marca o A partir de uma marca o inicial o comportamento representado pela movimenta o dos to kens ao longo do grafo Tal acontece em resultado do disparo 8 das transi es que se encontrem em condi es de o fazer i habilitadas o que acontece se todos os seus lugares antecessores ou de entrada possuirem tokens O disparo de uma transi o ou seja a sua activa o implica a remo o dos tokens dos lugares de entrada da transi o e a sua passagem para os lugares sucessores Em cada momento
54. obre Formal Language Description Languages bem como o curso do laborat rio de Viena da IBM sobre Sem ntica das Linguagens de Programa o ambos em 1965 4type checking CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 72 impl cita outra caracter stica t pica e de complexo tratamento matem tico Finalmente as linguagens imperativas basei am se na no o de vari vel de valor mut vel no tempo atrav s de uma instru o de atribui o e na passagem de par metros por refer ncia associando dois identificadores mesma quantidade Perdem assim de forma definitiva uma propriedade crucial em matem tica a transpar ncia referencial A consequ ncia imediata da n o obedi ncia a esta propriedade nas linguagens imperativas a possibilidade de surgirem nos programas efeitos laterais que para al m de pre judicarem a qualidade intr nseca do mesmo em termos de legibilidade modula ridade etc s o de dif cil tratamento matem tico Esta discrep ncia entre a linguagem de programa o cuja sem ntica se pretende definir e a metalinguagem matem tica de defini o levou muitos autores a tentarem definir novas linguagens que por serem matematicamente bem fundadas prescindiram da metalinguagem S o hoje exemplos cl ssicos o Lisp McCarthy 62 com base na teoria das fun es recursivas e no calculus Church 41 o Prolog Colmerauer et al 79 Warren 77 baseado nos trabalhos sobre mecaniza o da l gica re
55. omo os seus custos s o hoje em dia factos bem reconheci dos ainda que a pr tica n o tenha sido substancialmente alterada 17 debugging 18 cf a c lebre frase o teste de um programa apenas pode demonstrar a exist ncia de erros nunca a sua aus ncia CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 80 Taxonomia de M todos de Verifica o Bases Fundamentais Sem ntica via Espa os de Estados Defini o da fia Abordagens Verifica o M todos de Verifica o de Programas Correc o Parcial Correc o Total Segu nciais Comec o Total de Programas Paralelos Paralelas Fig 3 4 Taxonomia da Verifica o de Programas Outras t cnicas informais de tipo est tico como por exemplo as phased ins pections Knight e Myers 93 t m surgido como complementares aos testes no exemplo em refer ncia apoiada at por uma ferramenta em computador No entanto e como salienta Grady num interessante e actual estudo sobre a qualidade do software Grady 93 a boa qualidade do software o resultado da boa qualidade da Engenharia da Programa o sendo a qualidade desta de pendente do rigor colocado no processo A verifica o est tica e formal da correc o de programas a alternativa rigorosa apontada A verifica o consiste numa prova matem tica de satisfa o onde se procura provar que o programa P uma vez definido matematicamente o seu signif
56. pecifica es por modelos O m todo de refinamento designado por refinamento progressivo33 pois prop e que em sucessivos passos os tipos matem ticos usados como modelos na especifica o sejam reificados i materializados em representa es mais concretas no sentido da implementa o sendo as opera es de seguida refina das de acordo com a reifica o de dados tal como se ilustra na figura 3 6 Especifica o provas de correc o Reifica o Refinamento Opera es Fun es Refinadas Tipos Reificados D Fun es da Implementa o Tipos da Implementa o Implementa o Final Fig 3 6 O M todo VDM Em cada passo de reifica o de dados escrevem se as designadas fun es de retrieve ou de recupera o de abstrac o que tornam poss vel provar que todos os valores abstractos s o represent veis pelo tipo reificado designando se esta prova por prova de adequa o Outras provas sobre as opera es refina das s o realizadas tais como a garantia da preserva o dos invariantes defini dos a este n vel 33 stepwise refinement CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 96 As provas de correc o em VDM realizam se usando c lculo de predicados indu o estrutural sobre os tipos matem ticos e um esquema de prova baseado no estilo l gico da dedu o natural Cada prova a realizar obedece a uma regra de pro
57. plo para a instru o com posta S So composi o sequencial tem se P Sy R R So Q P S1 So Q 13 flowcharts 14 O requisito de composicionalidade nos m todos de verifica o relevante dada a sua extens o aos m todos de especifica o CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 78 Para al m de apenas ter a possibilidade de verificar correc o parcial ou seja n o cobrindo a prova da termina o do programa outro dos identificados grandes problemas do m todo consiste na dificuldade de se encontrarem as asser es correctas Floyd j havia identificado este problema tendo sugerido regra de infer ncia para a frente i no sentido antecedente consequente Segundo esta regra partindo de uma asser o escrita antes de uma instru o o problema consiste em encontrar a mais forte asser o verdadeira ap s a exe cu o dessa instru o ou seja o mais forte consequentes verific vel 5 Mais tarde o pr prio Floyd e outros investigadores cf King 69 reconhece ram as dificuldades deste esquema de infer ncia pelo que uma regra de infe r ncia mais simples usando infer ncia para tr s foi definida e utilizada pelo pr prio Hoare no seu trabalho Posteriormente Dijkstra em Dijkstra 74 que sugere um m todo mais preciso ao associar p s condi o n o uma qualquer pr condi o mas a do ponto de vista l gico mais fraca pr condic o escrita co
58. resentados no mbito do trabalho para a standardiza o do m todo de signadamente Fitzgerald e Jones 90 Middelburgh 90 e Fitzgerald 91 VDM um m todo bem fundamentado de especifica o por modelos tendo originado muitas ideias que podem ser utilizadas por outras abordagens seme lhantes designadamente quanto base matem tica das provas Destas outras escolas de especifica o por modelos seria uma omiss o grosseira a n o refer ncia escola de Oxford e linguagem de especifica o Z Spivey 89 a desenvolvida A linguagem Z procurando ser mais uma linguagem de descri o do que uma base de desenvolvimento por refinamento coloca uma nfase maior na prova do que numa poss vel constru o de prot tipos ou at esquema de refinamento De base l gica tal como Meta IV a linguagem Z oferece um exagerado grau de liberdade quanto forma de especifica o de dados e de opera es Ainda que os tipos matem ticos sejam os mesmos que se apresentaram atr s em rela o a VDM o mecanismo b sico de constru o de especifica es em Z designa se CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 97 esquema t sendo usado para representar dados e suas propriedades ou apenas opera es ou a composi o destas seguindo uma linguagem de esquemas igualmente dispon vel Hayes 87 n o existindo claramente a no o de estado Por exemplo a declara o do tipo Queue seria neste caso feita usando o es qu
59. ritos Da que igualmente bastante cedo anos 60 ainda que em paralelo apare am referidas na literatura confer ncias e cursos sobre descri o formal de linguagens de programa o Embora a maioria dos esfor os na forma liza o de linguagens de programa o n o tenham tido a ver directa e imediata mente com preocupa es de verifica o dos programas mas antes com a cons tru o de compiladores mais eficientes o resultado observ vel uma influ ncia m tua entre as reas ainda que mais no sentido da sem ntica das linguagens para os m todos de verifica o do que no sentido contr rio pois poucas foram as linguagens definidas tendo por objectivo facilitar a verifica o formal da correc o dos programas nelas escritos ainda que regras para tal fossem j co nhecidas Tennent 77 Escrito um programa numa qualquer linguagem de programa o a determi na o matem tica do seu significado indispens vel para a posterior avalia o da sua correc o passa pela defini o formal da sintaxe e sem ntica est tica ou din mica de tal linguagem de programa o A sintaxe seja mais abstracta ou mais concreta descreve a estrutura correcta dos programas numa perspectiva gramatical A sem ntica est tica des creve restri es estruturais tais como regras de verifica o de tipos4 em geral n o adequadamente descritas pelos usuais formalismos sint cticos ditos inde pendentes do contexto estabelecendo pois rela es
60. s bem como a inexist ncia de um estado expl cito tem a vantagem de permitir que se definam TAD em completo afastamento de preo cupa es de implementa o e portanto de forma bastante abstracta A reescrita ser o mecanismo fundamental para que se realizem c lculos e provas sobre termos sempre com base nos axiomas Em certos casos por m a n o exist ncia de um modelo expl cito torna as especifica es complexas Por exemplo cf Loeckx 87 a defini o alg brica de um conjunto matem tico obrigando garantia de inexist ncia de duplicados torna a sua especifica o alg brica dif cil usando um conjunto finito de axiomas Uma solu o comum para tal tipo de problemas a considera o de um conjunto de opera es privadas sobre o TAD definidas pelo especificador e posteriormente n o acess veis ao utilizador da implementa o do mesmo que funcionam como predicados que garantem propriedades a serem observadas por qualquer implementa o do TAD e que na abordagem alg brica s o designados por operadores escondidos3 que s o o equivalente alg brico aos predicados que na abordagem por modelos como veremos a seguir se designam invariantes A abordagem alg brica favorece como se pode verificar pelo exemplo dado n veis de abstrac o e de formaliza o elevados Do ponto de vista da utiliza o pr tica das especifica es alg bricas ou at do seu ensino este elevado grau de formaliza o tem implica
61. s o uma outra classe de formalismos para especifica o de sistemas concorrentes cujos exemplares mais referenciados s o CSP Hoare 85 e CCS Milner 89 de base te rica alg brico denotacional A complexidade te rica de uma caracteriza o formal destes m todos associada ao facto de n o serem estritamente relevantes no contexto desta tese leva nos a n o omitindo a sua refer ncia n o realizar a sua apresenta o aprofundada lgebras de processos representam os comportamentos de agentes cf CCS ou processos cf CSP sob a forma de termos de uma lgebra estendida com duas esp cies representativas de ac es ou eventos e de comportamentos e de um conjunto de combinadores ou ainda sob a forma de um conjunto de asser es sobre os elementos da lgebra CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 103 Diversos modelos sem nticos interpretados em diferentes l gicas condu zem a distintas sem nticas comportamentais Estas abordagens possuem uma s lida base formal e tratamento matem tico adequado tendo ainda caracter sticas de composicionalidade indispens veis para a sua utiliza o em especifica es A ocorr ncia de eventos em geral considerada instant nea n o existindo a no o de causalidade entre eventos A possibilidade de se determinar em que circunst ncias dois processos s o equivalentes em geral tratada de forma diferente Por exemplo em CSP dois processos s o equivalentes
62. s vel ainda que seja uma condi o necess ria mas n o sufici ente no julgamento final da qualidade de um programa dado que como sabe mos avalia es de usabilidade realizadas pelos utilizadores podem ser decis rias Relembra se a prop sito que esta tese se situa exactamente na conver g ncia das duas propriedades t o procuradas Sendo uma condi o necess ria a correc o dos programas deve portanto merecer e assim tem acontecido desde os prim rdios da computa o uma aten o particular quer na sua defini o substantiva quer na consequente procura de m todos para a sua rigorosa verifica o A verifica o da correc o de um programa ou aplica o est ligada verifica o de dois requisitos b si cos a termina o e a satisfa o dos requisitos A conjun o destas duas proprie dades designa se por correc o total que o m nimo exig vel Apesar do desenvolvimento de programas ser uma actividade criativa rigor um complemento indispens vel pois s atrav s de abordagens rigorosas se podem produzir produtos mais fi veis Por m rigor ainda assim uma propri edade intuitiva e n o defin vel de forma rigorosa Para al m disso v rios n veis de rigor podem ser estabelecidos e atingidos sendo o mais alto n vel de rigor o que se designa por formaliza o 2 tradu o corrente do termo ingl s usability CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 70 Sendo os programas
63. s os estados antes e ap s a sua execu o CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 93 Analisemos agora a especifica o por modelos do TAD Queue anteriormente especificado algebricamente para melhor se verem as diferen as entre os dois m todos Comecemos pr tentar encontrar um modelo matem tico que possa ser apropriado representa o abstracta de uma fila de espera dentre os que usualmente fazem parte do leque de modelos matem ticos oferecidos por estes m todos designadamente conjuntos sequ ncias fun es finitas 2 tuplos e rela es bin rias O tipo Queue representar o estado interno da fila de espera e sendo uma fila de espera uma estrutura linear uma sequ ncia ser utilizada Utilizou se no exemplo um estilo funcional na especifica o das opera es sobre uma fila de espera ainda de notar que a linguagem matem tica usada na especifica o das fun es tem que ser adequada aos modelos matem ticos que s o argumen tos destas Escolhida uma sequ ncia de objectos para modelar a fila de espera n o ser de estranhar que qualquer manipula o da fila de espera deva ser especificada usando as fun es sobre sequ ncias definidas na linguagem QUEUE Estado Queue Elem Elem Nat inv Queue g len q lt 200 opers initq queue inicializa o initg lt gt enqueue queue x elem queue inser o enqueue g e q lt e gt dequeue qu
64. scri es realizadas a possibilidade de se utilizar a t cnica de prototipagem r pida tida por alguns Hartson e Smith 87 como meio ideal de di logo com o cliente ou o utilizador para afina o de requisitos uma vantagem que em muito pode influenciar na escolha do forma lismo a empregar As principais caracter sticas dos principais m todos formais de especifica o s o a seguir apresentadas 3 4 M todos Formais de Especifica o Ainda que os m todos formais de especifica o venham sendo aplicados em m ltiplos contextos como por exemplo a especifica o de VLSI de protocolos de redes de interfaces com o utilizador ou de certos componentes de aplica es multi m dia os m todos formais que nos interessa aqui CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 87 considerar s o os actualmente dispon veis para a especifica o dos requisitos funcionais de sistemas software Estes m todos t m vindo a ser classificados com grau de rigor e amplitude diferente conforme os autores e a sua perspectiva Cohen et al 86 Davis 88 sendo certo que quase imposs vel encontrar uma classifica o suficientemente disjunta para que seja absolutamente clara No entanto duas perspectivas parecem ser indispens veis designadamente a que privilegia a funcionalidade interna ou comportamento interno e a que tem por vis o predominante a funcionalidade externa ou seja o comportamento que pode ser externam
65. sibilidade de cria o autom tica de prot tipos que podem ser mesmo processos UNIX comunicando atrav s de canais bem definidos Possibilidade de se criarem em fases muito iniciais do processo de con cep o simuladores das aplica es ligando o c digo do prot tipo a uma camada interactiva Simuladores que podem e devem at ser considerados como referenciais para efeitos contratuais TItera o e ciclos de desenvolvimento que podem ser realizados volta da especifica o formal e do simulador C lculo rigoroso e gradual da implementa o final que substitui a tradici onal prova de correc o suportado pelas ferramentas de constru o de prot tipos que possibilitam fases h bridas ou seja fases em que o c digo do prot tipo coexiste com por es j constru das da aplica o Produ o sistem tica da documenta o de projecto Para terminar refira se que ao rigor e sistematiza o do processo de cons tru o da camada computacional n o corresponde por m igual m todo siste matiza o ou automatiza o na constru o da camada interactiva Porque esse o problema para o qual se procuram nesta tese solu es ainda que com preo cupa es adicionais de generalidade a abordagem CAMILA SETS pode ser consi derada uma potencial cliente dessas solu es CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 107 3 6 Sum rio Neste cap tulo foi feita uma apresenta o a
66. tica Translacional 7 por exemplo uma m quina de reescrita ou uma m quina de stack 8V ienna Definition Language 9 V ienna Devdopment M ethod CAP TULO 3 M TODOS FORMAIS EM ENG DA PROGRAMA O 74 A ideia base da sem ntica translacional Stell 66 exprimir a sem ntica das constru es de uma linguagem usando um esquema de tradu o que para cada programa escrito na linguagem original realiza a sua tradu o para uma outra linguagem mais simples mais compreens vel mais trat vel em suma De notar que a sem ntica da linguagem se encontra especificada na desi gnada fun o de tradu o conforme se ilustra na figura 3 2 Programa Fonte Fun o de Tradu o Dados de Entrada Programa Objecto Execu o Resultados Fig 3 2 Sem ntica Translacional Ainda que um tal esquema de tradu o possa ser interessante para a futura constru o de compiladores da linguagem dado definir todas as fun es de tradu o que o compilador dever implementar caso se use a mesma linguagem objecto esta abordagem apresenta insufici ncias resultantes da sua falta de abstrac o da sua intr nseca depend ncia da linguagem objecto e mais impor tante ainda por ser recorrente dada a necessidade de igualmente se prover a linguagem objecto de uma sem ntica formal Estas inefici ncias da abordagem conduziram ao seu quase completo abandono Gram ticas de Atributos Especifica es gramatica
67. tti Marchetti 81 a passa gem da fase emp rica fase de teoriza o visando atingir a automatiza o Em s ntese a credibilidade e evolu o da Engenharia da Programa o muito tem a ver com o rigor e formalidade dos seus modelos m todos e t cnicas para al m dos princ pios espec ficos que possam ser encontrados Resultados foram entretanto sendo conseguidos que vieram trazer algum desenvolvimento rea No mbito do generalizado modelo imperativo s o de referir os desenvolvimentos relativos ao c digo tais como a programa o estrutu rada Dijkstra 76 a programa o modular Parnas 72 as linguagens com disci plina forte de tipos e as linguagens modulares No mbito do tratamento intensi vo de informa o processamento de dados o modelo relacional de bases de da dos Codd 70 de base formal foi decisivo para se atingir o grau de automatiza o hoje em dia existente em tal rea Numa outra linha de evolu o que mais nos interessa aqui considerar a necessidade sentida por alguns de tratar o c digo ou programas fonte como objectos de car cter matem tico conduziu ao aparecimento de paradigmas e linguagens de programa o de base matem tica sendo de salientar as lingua gens funcionais como Lisp McCarthy 62 MIRANDA Turner 85 ou ML Harper 86 de base l gica como o Prolog Warren 77 Colmerauer et al 79 e de base alg brica como o OBJ Goguen e Meseguer 82 Programas escritos nestas linguage
68. ulo de weakest preconditions introduzindo a no o de invariante de abstrac o Os c lculos de Oxford e SETS possuem al guma rela o na medida em que o que o primeiro assume como heur stica a de termina o dos invariante de abstrac o que o segundo calcula A tabela seguinte sintetiza as diferentes classes de abordagens verifica o da correc o de programas nesta sec o referidas Testes Determina o da Correc o Inspec es de Programas a posterior Verifica o Construtiva C lculo Tab 3 2 Valida o de Programas 3 2 3 Tipos Abstractos de Dados Desde os anos 70 que aquando do aparecimento das primeiras linguagens com disciplina forte de tipos a no o de tipo de dados foi associada no o mate m tica de conjunto de valores em aceit vel sintonia com a corrente ent o predo minante que privilegiava a separa o entre dados e instru es Assim as opera es pass veis de serem realizadas sobre os valores de um tipo de dados n o fa ziam parte da sua defini o Morris em Morris 73 considera que o modelo adequado para representar matematicamente um tipo de dados uma lgebra concreta e n o um conjunto e que portanto ao conjunto de valores deve ser associado o conjunto de opera dores que os manipulam Esta ideia te rica era suportada na pr tica pelo que havia j sido consegui do no mecanismo class2 da linguagem Simula 67 Dahl 68
69. va bem definida restando o nus do tratamento matem tico Um exemplo bastante completo quanto estrita aplica o do m todo pode ser encontrado em Fielding 80 A linguagem de especifica o usada em VDM a linguagem Meta IV Bj rner e Jones 82 linguagem que possui uma sem ntica denotacional que lhe confere o valor de um formalismo de descri o de significado preciso No entan to a linguagem n o execut vel o que impede a constru o de prot tipos Po r m in meras ferramentas foram desenvolvidas quer de apoio s especifica es quer de apoio s provas Procurando juntar ao rigor do m todo a possibilidade da cria o de prot ti pos algumas linguagens de especifica o por modelos execut veis foram criadas em particular metoo Henderson e Minkowitz 86 e posteriormente CAMILA Almeida e Barbosa 91 esta desenvolvida na Universidade do Minho Na sua vers o actual VDM um m todo bem reconhecido em particular na rea da especifica o de sistemas de informa o sequenciais depois de ter sido utilizado no contexto da IBM para a especifica o de linguagens como ADA e CHILL e em muitos outros projectos industriais encontrando se em fase de standardiza o Ainda que seja um m todo construtivo VDM n o tem a si associados de base mecanismos particulares para a composi o modular de especifica es Alguns esfor os nesse sentido t m vindo a ser realizados sendo de salientar os que t m sido ap
70. volvimentos na rea espec fica da sem ntica das linguagens e dos processadores das mesmas bem como extens es de grande sucesso na rea dos editores estruturados Reps e Teitelbaum 88 n o nos parece de grande utilidade neste contexto introduzir mais detalhe sobre esta abordagem podendo descri es mais completas ser encontradas em Waite e Goos 84 Deransart et al 88 e Henriques 92 Sem ntica Denotacional A abordagem denotacional tal como a translacional baseia se na defini o da sem ntica de uma linguagem de programa o atrav s de um esquema de tradu o que associa um significado denota o a cada constru o da linguagem Scott 70 Tennent 76 Stoy 77 Por m enquanto que na abordagem transla cional o resultado da tradu o um programa nesta abordagem tal resultado um objecto matem tico a denota o O da constru o o que de imediato evita o problema de circularidade atr s referido A descri o denotacional de uma linguagem de programa o consiste na defini o de um conjunto de fun es de significadoll que estabelecem as corres pond ncias entre as constru es sint cticas e os dom nios sem nticos 2 ap s devida classifica o destes sendo as fun es significado indexadas pela classe das constru es sint cticas que traduzem Genericamente assumem a forma matem tica de uma fun o que estabelece uma correspond ncia de um para um entre cada dom nio sint ctico

capítulo 3 métodos formais

Contents

Download Pdf Manuals

Related Search

Related Contents

cap&iacute;tulo 3 m&eacute;todos formais

Contents

Download Pdf Manuals

Related Search

Related Contents

capítulo 3 métodos formais