UMA PROPOSTA PARA ESPECIFICAÇÃO DE OBJETOS FUNCIONAIS EM LINGUAGEM Z PARA UTILIZAÇÃO EM UM ARCA*

UMA PROPOSTA PARA ESPECIFICAÇÃO DE OBJETOS FUNCIONAIS EM LINGUAGEM Z PARA UTILIZAÇÃO EM UM ARCA*

Duarte, Glaucius D.; Dimuro, Graçaliz P.; Costa, Antônio Carlos da Rocha

Escola de Informática - ESIN/UCPel

Universidade Católica de Pelotas

Última alteração: 21/01/2000 às 11:01

* ARCA (Ambiente de Realidade Virtual Cooperativo de Aprendizagem)

Story board - ARCA ( sugerido em [NIT 1999] )

Autor: Julio Nitzke (UFRGS)

Linguagem Z

- linguagem utilizada para especificação de sistemas de software, a partir da utilização de métodos formais;

- notação desenvolvida pelo Grupo de Pesquisas em Programação da Universidade de Oxford (em 1994);

- fundamenta-se na construção de esquemas, que salientam a importância de determinados elementos do sistema de software, além de fazer algumas declarações sobre as relações existentes entre estes elementos;

- não é uma notação executável. Todavia muitas especificações de Z (de funcionalidade ou modelos da área de assunto) podem ser traduzidas de um modo bastante direto em um idioma executável, como Prolog.

- uma especificação em Z declara fatos sobre o sistema de uma maneira clara, o que torna possível usar Z para gerar informação sobre o código.

Definições Globais ( a partir de [NIT 1999], [TAR 1999] )

Fundamentação teórica de Z em:

[BAR 1994], [RAN 1994], [WOD 1996], [WOR 1996]

ELETRODOMÉSTICOS ::= refrigerador | freezer

INSTRUMENTOS ::= relógio | calendário | panela e fogão | faca

CONDIÇÕES_AMBIENTAIS ::= ambiente

LEGUMES ::= batata

FORMAS_DE_CORTAR == {"não cortar e nem remover a casca", "cortar a casca",

"cortar em pedaços"}

TIPO_DE_COZIMENTO == {"nenhum cozimento", "leve", "prolongado"}

GRAUS_CELSIUS == {x : R | -19 < x < 41}

DIAS == {x : N | 0 < x < 366}

MINUTOS == { x : N | 0 < x < 1440}

Descrição 1: No refrigerador a temperatura é normalmente ao redor de 4 ^oC. Algumas reações prováveis nestas condições: ... deverá ocorrer perda de vitamina C ... .

Resfriamento

_resfria_ : ELETRODOMÉSTICOS « LEGUMES

temperatura_de_resfriamento? : GRAUS_CELSIUS

temperatura_de_resfriamento? = {4}

refrigerador batata

reply! = {"perda de vitamina C"}

Descrição 2: No freezer a temperatura é normalmente ao redor de –18 ^oC. Algumas reações prováveis nestas condições: ... a estrutura do produto modifica-se, pois ele congela – a modificação é diferente se o produto for cozido ou não .... deverá ocorrer uma leve perda de vitamina C ... .

Congelamento

_congela_ : ELETRODOMÉSTICOS « LEGUMES

temperatura_de_congelamento? : GRAUS_CELSIUS

temperatura_de_resfriamento? = {-18}

freezer batata

reply! = {"perda de vitamina C", "alimento congela", "estrutura do alimento modifica-se"}

Descrição 3: A mesa simboliza deixar o produto a temperatura ambiente, que pode variar de acordo com a estação do ano indicada pelo calendário. Algumas reações prováveis nas condições normais (± 20 ^oC): ... poderá ocorrer uma perda de vitamina C ... .

Alteração de Temperatura

_altera_temperatura_ : CONDIÇÕES_AMBIENTAIS « LEGUMES

temperatura_ambiente? : GRAUS_CELSIUS

temperatura_ambiente? Î ran (GRAUS_CELSIUS > 19...21)

ambiente batata

reply! = {"perda de vitamina C"}

Descrição 4: No freezer a temperatura é normalmente ao redor de –18 ^oC. Algumas reações prováveis nestas condições: ... microbiologicamente o produto pode permanecer sem alterações por cerca de 6 a 8 meses ... .

Congelamento X Tempo Decorrido

_congela_ : ELETRODOMÉSTICOS « LEGUMES

_envelhece_ : INSTRUMENTOS « LEGUMES

temperatura_de_congelamento? : GRAUS_CELSIUS

tempo_em_dias? : DIAS

(temperatura_de_congelamento? = {-18}

freezer batata)

(tempo_em_dias? Î ran (DIAS > 0...240)

calendário batata)

reply! = {"sem alterações"}

Descrição 5: No refrigerador a temperatura é normalmente ao redor de 4 ^oC. Algumas reações prováveis nestas condições: ... microbiologicamente o produto pode permanecer sem alterações por cerca de 2 a 3 meses, após este tempo pode começar a desenvolver alguns mofos e germinar, e posteriormente apodrecer devido a presença de mofos e bactérias ... .

Resfriamento X Tempo Decorrido

_resfria_ : ELETRODOMÉSTICOS « LEGUMES

_envelhece_ : INSTRUMENTOS « LEGUMES

temperatura_de_resfriamento? : GRAUS_CELSIUS

tempo_em_dias? : DIAS

(temperatura_de_resfriamento? = {4}

refrigerador batata)

(tempo_em_dias? Î ran (DIAS > 241...1440)

calendário batata)

reply! = {"desenvolve mofo", "germina", "ação das bactérias", "apodrece"})

Descrição 6: O fogão poderá ser usado em conjunto com a panela para cozer levemente, ,cozer bem ou se quisermos complicar um pouco mais fritar as batatas. Caso o cozimento seja leve: ... teremos uma diminuição do escurecimento enzimático durante a armazenagem em refrigerador ou freezer ... . Caso o cozimento seja prolongado: ... não deverá quase ocorrer escurecimento enzimático durante a armazenagem em refrigerador ou freezer ... a diminuição da concentração microbiana e a perda de vitmina C serão maiores com uma alteração significativa na vida de prateleira do produto tanto no freezer como no refrigerador ... .

Cozimento X Congelamento

_cozinha_ : INSTRUMENTOS « LEGUMES

_congela_ : ELETRODOMÉSTICOS « LEGUMES

cozimento? : TIPO_DE_COZIMENTO

temperatura_de_congelamento? : GRAUS_CELSIUS

((cozimento? = {"leve"}

panela_e_fogão batata)

(temperatura_de_congelamento? = {-18}

freezer batata)

reply! = {"diminuição do escurecimento enzimático"})

((cozimento? = {"prolongado"}

panela_e_fogão batata)

(temperatura_de_congelamento? = {-18}

freezer batata)

reply! = {"não deverá quase ocorrer escurecimento enzimático", "maior diminuição da

concentração microbiana", "maior perda de vitamina C", "alteração significativa na

vida de prateleira do produto"})

Descrição 7: A mesa simboliza deixar o produto a temperatura ambiente, que pode variar de acordo com a estação do ano indicada pelo calendário. Algumas reações prováveis nas condições normais (± 20 ^oC): ... microbiologicamente o produto pode permanecer sem alterações por cerca de 1 mês, após este tempo pode começar a desenvolver alguns mofos ou germinar, e posteriormente apodrecer devido a presença de mofos e bactérias ... .

Alteração da Temperatura Ambiente X Tempo Decorrido

_altera_temperatura_ : CONDIÇÕES_AMBIENTAIS « LEGUMES

_envelhece_ : INSTRUMENTOS « LEGUMES

temperatura_ambiente? : GRAUS_CELSIUS

tempo_em_dias? : DIAS

((temperatura_ambiente? Î ran (GRAUS_CELSIUS > 19...21)

ambiente batata)

(tempo_em_dias? Î ran (DIAS > 1...30)

calendário batata)

reply! = {"sem alterações"})

((temperatura_ambiente? Î ran (GRAUS_CELSIUS > 19...21)

ambiente batata)

(tempo_em_dias? Î ran (DIAS > 31...1440)

calendário batata)

reply! = {"desenvolve mofo", "germina", "ação das bactérias", "apodrece"})

Descrição 8: A mesa simboliza deixar o produto a temperatura ambiente, que pode variar de acordo com a estação do ano indicada pelo calendário. Algumas reações prováveis nas condições normais (± 20 ^oC): ... caso o produto esteja descascado ou cortado em pedaços e não tenha tido nenhum cozimento leve irá começar a ocorrer um escurecimento enzimático após uma ou duas horas ... .

Temperatura Ambiente X Tipo de Corte X Tempo Decorrido

_altera_temperatura_ : CONDIÇÕES_AMBIENTAIS « LEGUMES

_corta_ : INSTRUMENTOS « LEGUMES

_envelhece_ : INSTRUMENTOS « LEGUMES

temperatura_ambiente? : GRAUS_CELSIUS

tipo_de_corte? : FORMAS_DE_CORTAR

tempo_em_minutos? : MINUTOS

((temperatura_ambiente? Î ran (GRAUS_CELSIUS > 19...21)

ambiente batata)

(tipo_de_corte? Í {"cortar a casca", "cortar em pedaços"}

faca batata)

(tempo_em_minutos? Î ran (MINUTOS > 60...1440)

relógio batata)

reply! = {"escurecimento enzimático"})

Descrição 9: No refrigerador a temperatura é normalmente ao redor de 4 ^oC. Algumas reações prováveis nestas condições: ... caso o produto esteja descascado e não tenha tido um cozimento leve antes de ser armazenado poderá ocorrer um escurecimento enzimático após dois ou três dias ... .

Tipo de Corte X Cozimento X Resfriamento X Tempo Decorrido

_resfria_ : ELETRODOMÉSTICOS « LEGUMES

_cozinha_ : INSTRUMENTOS « LEGUMES

_corta_ : INSTRUMENTOS « LEGUMES

_envelhece_ : INSTRUMENTOS « LEGUMES

temperatura_de_resfriamento? : GRAUS_CELSIUS

cozimento? : TIPO_DE_COZIMENTO

tipo_de_corte? : FORMAS_DE_CORTAR

tempo_em_dias? : DIAS

((tipo_de_corte? = {"cortar a casca"}

faca batata)

(cozimento? = {"nenhum cozimento"}

panela_e_fogão batata)

(temperatura_de_resfriamento? = {4}

refrigerador batata)

(tempo_em_dias? Î ran (DIAS > 2...360)

calendário batata)

reply! = {"escurecimento enzimático"})

Descrição 10: A faca é um instrumento opcional para cortar a batata em fatias ou descascá-la, com o que alteram-se todas as reações nas outras condições: ... com a batata em pedaços menores ou descascada ela cozinha mais rápido, escurece mais rapidamente e perde mais vitamina C ... .

Tipo de Corte

_corta_ : INSTRUMENTOS « LEGUMES

tipo_de_corte? : FORMAS_DE_CORTAR

tipo_de_corte? Í {"cortar a casca", "cortar em pedaços"}

faca batata

reply! = {"cozinha mais rápido", escurece mais rapidamente", "perde mais vitamina C", "aceleração

do crescimento microbiano"}

Descrição 11: O fogão poderá ser usado em conjunto com a panela para cozer levemente, cozer bem ou se quisermos complicar um pouco mais fritar as batatas. Caso o cozimento seja leve: ... a estrutura não modificará muito ... a diminuição da concentração microbiana e a perda de vitamina C serão pequenas ... não altera significativamente a vida de prateleira do produto ... . Caso o cozimento seja prolongado: ... a estrutura pode modificar drasticamente ... .

Cozimento

_cozinha_ : INSTRUMENTOS « LEGUMES

cozimento? : TIPO_DE_COZIMENTO

((tipo_de_cozimento? = {"leve"}

panela_e_fogão batata)

reply! = {"a estrutura do alimento não sofrerá grandes alterações", "leve redução da

concentração microbiana", "leve perda de vitamina C", "nenhuma alteração

significativa na vida de prateleira do alimento"})

((tipo_de_cozimento? = {"prolongado"}

panela_e_fogão batata)

reply! = {"a estrutura do alimento pode modificar drasticamente"})

Referências Bibliográficas:

[BAR 1994] BARDEN, R.; Stepney, Susan; Cooper, David. Z In Practice. New York, Prentice Hall, 1994.

[NIT 1999] NITZKE, Julio Alberto. Story board - ARCA. Documento disponível na Internet em Dezembro/1999 no endereço http://penta.ufrgs.br/~julio/arca .

[RAN 1994] RANN, David; Turner, John; Whitworth, Jenny. Z: A Beginner´s Guide. London, Chapman & Hall, 1994.

[TAR 1999] TAROUCO, Liane M. R. & outros. Projeto ARCA - Ambiente de Realidade Virtual Cooperativo de Aprendizagem. Documento disponível na Internet em Dezembro/1999 no endereço http://penta.ufrgs.br/pgie/arca/arca.htm .

[WOD 1996] WOODCOCK, Jim; Davies, Jim. Using Z - Specification, Refinement, and Proof. London, Prentice Hall, 1996.

[WOR 1996] WORDSWORTH, J. B. Software Development with Z - A Practical Approach to Formal Methods in Software Engineering. Harlow, Addison-Wesley, 1996.