Introdução à Abstração de Dados

Autor(es): Daltro J. Nunes
Visualizações: 213
Classificação: (0)

Trata-se de um livro que ensina a especificar, ou modelar, soluções de problemas computacionais em alto nível de abstração e a desenvolver o raciocínio algorítmico. Para especificar soluções de problemas, o livro utiliza uma linguagem de programação funcional denominada MAuDE. Assim, a atividade de especificação ou modelagem da solução de problemas torna-se prazerosa e gratificante, pois as especificações são interpretáveis (executáveis) em qualquer computador, permitindo testá-las quanto a sua corretude.

FORMATOS DISPONíVEIS

eBook

Disponível no modelo assinatura da Minha Biblioteca

12 capítulos

Formato Comprar item avulso Adicionar à Pasta

Capítulo 1 - Especificação de tipos primitivos: tipo TRUTH-VALUES

PDF Criptografado

capítulo

1

especificação de tipos primitivos tipo TRUTH-VALUES

■ ■

1

A computação usa de forma recorrente o conceito matemático de álgebra1 para formalizar sua ciência: máquinas, gramática, autômatos, métodos formais, processos, banco de dados, software, hardware, etc. Entretanto, em vez de definir, na formalização, uma

álgebra diretamente, pode-se fazer uso de uma linguagem que a descreve. Os “programas” dessa linguagem são chamados de especificações algébricas.

Essa linguagem pode ser usada, também, com grandes vantagens para especificar tipos de dados, como visto na introdução, pois existe uma relação quase direta entre tipo de dado e álgebra.

Mais recentemente, tem-se usado também a teoria das categorias na modelagem.

2

Introdução à Abstração de Dados

A seguir, é visto o primeiro tipo de dado, o tipo TRUTH-VALUES2 (figura 1.1). A especificação algébrica começa pela palavra-chave3 fmod (módulo funcional), é seguida do nome do tipo que está sendo especificado, TRUTH-VALUES, e termina com a palavra chave endfm, sendo composta por duas partes: a primeira, chamada de assinatura, e a segunda, de sentenças4. Os conjuntos de valores5 são classificados em sortes e espécies6.

 

Capítulo 2 - Reescrita de termos

PDF Criptografado

capítulo

2

reescrita de termos

■ ■

Neste capítulo, é mostrado como equações podem ser usadas para transformar termos. Na computação, uma transformação pode ser vista como uma maneira de “calcular” uma função, uma expressão (corpo da função), fornecendo um resultado, um valor, quando não há, na expressão, ocorrências de variáveis. Usando o mesmo exemplo apresentado na secção 1.6 – conceito de equação, o valor da função f(x, y) = (x + y)/x, quando aplicada aos valores 3.0 e 6.0, é igual a 3.0. Informalmente, o processo de obtenção desse resultado é bem conhecido.

Comparando o termo f(x, y) com o termo f(3.0, 6.0), o valor 3.0 ocupa o lugar de x, e o valor 6.0 ocupa o lugar de y.

Logo, as variáveis que ocorrem na expressão devem ser também ocupadas pelos respectivos valores: (3.0 + 6.0)/3.0. Este capítulo tem como objetivo mostrar formalmente o processo de “calcular” um termo, possibilitando, assim, que ferramentas possam ser construídas.

20

 

Capítulo 3 - Extensão de tipos primitivos

PDF Criptografado

capítulo

3

extensão de tipos primitivos

■ ■

Este capítulo mostra como uma especificação pode ser estendida pela introdução de novos operadores, sem a necessidade de reeditar a especificação.

Por hipótese, uma especificação SPEC' define um novo sorte s. SPEC' tem operadores geradores e observadores da forma op f' : ... -> s .

Para expandir SPEC’ é necessário criar uma nova especificação SPEC e incluir SPEC’ em SPEC.

Em SPEC, novos operadores da forma op f : ...-> s . podem ser introduzidos.

Isso é possível graças à maneira como Maude trata as especificações que possuem inclusões, como mostrado a seguir.

38

Introdução à Abstração de Dados

As especificações são autocontidas, significando que têm todas as condições de reescrever qualquer termo gerado a partir de sua assinatura. Uma nova especificação tem um de dois objetivos:

1. definir um novo tipo de dado, podendo também estender tipos previamente especificados, como em NATURALS, visto a seguir; e

 

Capítulo 4 - Especificação de tipos primitivos: tipo NATURALS

PDF Criptografado

capítulo

4

especificação de tipos primitivos: tipo NATURALS

Este capítulo introduz o tipo de dado NATURALS.

O conjunto de valores deste tipo, comparativamente com o tipo TRUTH-VALUES, é infinito.

Ele “contém” o tipo THUTH-VALUES porque novos operadores do sorte Truth-Value são declarados e definidos.

Algumas equações deste tipo são recursivas, ou seja, são definidas em função delas mesmas.

É introduzido o conceito de equações condicionais, que podem ser aplicadas para reescrita somente se certas condições forem satisfeitas.

Finalmente, é mostrado como interpretar um sistema de equações como uma relação de congruência, ou seja, um sistema de equações denota uma relação de equivalência com uma propriedade adicional.

■ ■

46

Introdução à Abstração de Dados

O tipo NATURALS é caracterizado pelas operações zero 0, sucessor succ_, predecessor pred_, menor _<_, maior _>_, igual _ is_, adição _+_, multiplicação _∗_ e por um conjunto infinito de valores. Segue a especificação do tipo NATURALS: fmod NATURALS is

 

Capítulo 5 - Espécies

PDF Criptografado

capítulo

5

espécies

Este capítulo apresenta diversos recursos adicionais do Maude, aumentando a classe de problemas passíveis de solução. Os sortes podem ser estruturados em hierarquias de subsorte, sendo a relação de subsorte entendida como a inclusão de subconjuntos.

Inicialmente, é apresentado o conceito de inclusão de subsorte que tem um paralelo, na matemática, com inclusão de subconjuntos.

Chamando de Nat o sorte dos números naturais, Int o sorte dos números inteiros e Rat o sorte dos números racionais, a inclusão de subsorte Nat < Int < Rat indica que os números naturais estão contidos nos inteiros e esses por sua vez estão contidos nos racionais. A inclusão de subsorte

é declarada usando a palavra-chave subsort.

A declaração da inclusão de subsorte subsort A < B estabelece que o sorte A é um subsorte de B ou que A está incluído em B.

■ ■

62

Introdução à Abstração de Dados

Um conjunto de declarações de subsortes, sem ciclos,1 de uma especificação deve definir uma relação de ordem parcial ≤ sobre o conjunto de sortes declarados na especificação. ≤ é uma relação de subsorte e é uma forma de ordenar os subsortes (ordenamento de subsorte).

 

Capítulo 6 - Tipos parametrizados: sortes como parâmetros

PDF Criptografado

capítulo

6

tipos parametrizados: sortes como parâmetros

Um tipo de dado parametrizado é um modelo do qual podem ser obtidos tipos reais, usando os conceitos de teorias (fth) e instanciações (view). Neste capítulo, apenas sortes podem ser usados como parâmetro.

Tipos parametrizados também podem ser estendidos e sortes podem receber uma representação gráfica, que mostra como eles são organizados de forma hierárquica. Esta representação gráfica tem uma representação textual em Maude.

Também é mostrado, neste capítulo, como uma especificação pode ser estendida, mantendo-se ainda parametrizada.

Todos esses recursos são apresentados com a introdução de novos tipos de dados como

STACK, QUEUE, ARRAY, etc.

■ ■

88

Introdução à Abstração de Dados

Na especificação de tipos compostos, sortes do domínio das operações geradoras devem ser diferentes dos sortes de suas imagens. Assim, se op: s1 s2... si... sn -> s é uma geradora, pelo menos um sorte si deve ser diferente de s. Desta forma, os valores do novo sorte s são compostos por valores de outros sortes. As operações geradoras op encapsulam valores do sorte si, gerando valores do sorte s.

 

Capítulo 7 - Tipos parametrizados: termos como parâmetros

PDF Criptografado

capítulo

7

tipos parametrizados: termos como parâmetros

Termos podem, também, ser usados como parâmetros, potencializando as especificações de tipos parametrizados. Neste caso, uma teoria TH declara um operador f na forma

■ ■

op f : s1 ... si ... sn -> s .

e uma visão V que mapeia uma expressão f(..., x, ...), onde x é uma variável do sorte si,

em um termo t com ocorrências de variáveis x.

Uma especificação parametrizada pode ter ocorrências de um termo f(..., ti, ...), onde ti é um termo do sorte si.

O termo f(..., ti, ...) é, na instanciação, substituído por t[..., ti\x,...].

As especificações de P-STACK e SPARSE-ARRAY mostram a aplicação deste tipo de parâmetro.

140

Introdução à Abstração de Dados

Operadores formais op, declarados nas teorias TH, fth TH is

................. op op:..., si,... -> s.

................. endfth

onde si e s são sortes formais ou reais, podem ser mapeados, em uma visão V, para termos da assinatura de A-SPEC ou da assinatura de teorias,1 como mostrado na seguinte sintaxe: view 〈view-name〉

 

Capítulo 8 - Tipos parametrizados: operadores como parâmetros

PDF Criptografado

capítulo

8

tipos parametrizados: operadores como parâmetros

Operadores podem, também, ser usados como parâmetros, potencializando mais ainda as especificações de tipos parametrizados. Neste caso, uma teoria TH declara um operador formal op na forma

■ ■

op op : s1 ... si ... sn -> s .

e uma visão V mapeia o operador op no operador op’ de uma especificação A-SPEC.

Existem duas maneiras de fazer este mapeamento, causando efeitos diferentes. Equações formais podem ser declaradas nas teorias, estabelecendo propriedades do operador formal. No mapeamento, o operador op’ deve satisfazer essas propriedades. Como exemplos de aplicação, são mostradas as especificações

MAPPING, SET e BTREE. Visões entre teorias permitem instanciar especificações parametrizadas, mantendo-as ainda parametrizadas.

148

Introdução à Abstração de Dados

Operadores formais op, declarados nas teorias TH como fth TH is

................. op op: ..., si, ... -> s .

 

Capítulo 9 - Implementação abstrata de tipos abstratos de dados

PDF Criptografado

capítulo

9

implementação abstrata de tipos abstratos de dados

A especificação de um tipo de dado abstrato

SPEC pode ser “implementada” usando a especificação de outro tipo de dado X-SPEC.

A especificação SPEC’ é a especificação X-SPEC, estendida com as operações de SPEC.

Deve-se estabelecer uma correspondência entre os valores de SPEC’ e os valores de SPEC. Esta relação é uma função de abstração.

Assim, é possível provar que SPEC’ é uma implementação correta de SPEC.

Supondo que X-SPEC tenha uma implementação em alguma linguagem de programação, a implementação de SPEC’, na mesma linguagem,

é trivial.

■ ■

172

Introdução à Abstração de Dados

A “implementação” de tipos de dados deve ser entendida como o processo de criar representações. Por exemplo, se QUEUE' é uma representação de QUEUE, então QUEUE' se comporta como QUEUE, ou QUEUE' é uma implementação de QUEUE. Um tipo de dado é representado pela extensão de algum outro tipo. Por exemplo, QUEUE' é uma extensão do tipo LISTS e tem todas as operações do tipo QUEUE.

 

Capítulo 10 - Especificação algébrica e linguagens de programação

PDF Criptografado

capítulo

10

especificação algébrica e linguagens de programação

Este capítulo mostra como dar semântica a linguagens de programação, usando especificação algébrica.

Operações semânticas estabelecem uma relação entre sortes, s1, ..., sn, s, chamados domínios semânticos, dependente da sintaxe da linguagem de programação, Stx, interpretada como um conjunto de strings.

■ ■

operacao-semantica : Stx

s1 ...

sn -> s .

Para um programa prog escrito segundo a sintaxe da linguagem de programação Stx, Maude reduz o programa prog a um valor do sorte s. Ou seja, o resultado da computação de um programa é um valor do sorte s:

Maude> reduce operacao-semantica (prog, v1, ..., vn) onde v1, ..., vn são valores dos sortes s1, ..., sn, respectivamente.

186

Introdução à Abstração de Dados

Uma das aplicações da linguagem algébrica é seu uso na semântica de linguagens de programação (Mosses, 1992; Watt; Thomas, 1991). A seguir, é apresentada uma “pitadinha” desta aplicação.

 

Capítulo 11 - Álgebras

PDF Criptografado

capítulo

11

álgebras

Maude é uma linguagem de programação como Java, C, Haskell, ML.

Uma linguagem de programação é apenas um conjunto de strings, desprovido de significado, de semântica. A semântica de uma linguagem de programação

L é um mapeamento1 de L para algum conjunto da matemática (produto cartesiano, conjunto de funções, álgebras e outros.)

As especificações são strings da linguagem Maude.

É necessário, então, dar significado, semântica, a esses strings. As entidades matemáticas escolhidas para dar semântica às especificações são as álgebras. Por exemplo: TRUTH-VALUES pretende especificar uma

álgebra chamada álgebra Booleana. Assim, deve ser estabelecido um mapeamento entre TRUTH-VALUES e uma álgebra Booleana. Se esse mapeamento

é possível, a álgebra é o significado da especificação. Daí por diante, pode-se trabalhar somente a álgebra para definir e provar propriedades da especificação, algo que não pode ser feito com a própria especificação.

 

Capítulo 12 - Prova de teoremas

PDF Criptografado

capítulo

12

prova de teoremas

■ ■

Este capítulo não é absolutamente necessário para especificar tipos de dados, mas responde a muitas perguntas quanto ao aprofundamento dos capítulos anteriores.

Genericamente, uma equação t1 = t2 é uma relação de igualdade entre dois termos em Ts. É indiferente qual termo está no lado esquerdo ou direito.

Como visto, t ≡ t' é o enunciado de um teorema, ou seja, t ≡ t' = true, se o par 〈t, t'〉 está na relação de congruência.

220

Introdução à Abstração de Dados

Suponha uma especificação como TRUTH-VALUES, enriquecida com um conjunto de variáveis e sem nenhuma equação. Cada termo em Ts não possui qualquer relação com outro termo, exceto consigo mesmo (propriedade reflexiva). As classes de congruências (ver capítulo 11), neste caso, são formadas por cada termo em Ts.

Suponha que a especificação receba uma primeira equação not true = false

Seja t um termo em Ts com subtermos not true e false. Se t' é a reescrita de t, então t' está em Ts e tem false no lugar de um de seus subtermos not true ou not true no lugar de um de seus subtermos false. Tomando outros subtermos de t, pode-se obter, por reescrita, t", t'"... Conforme a definição da relação de congruência (ver capítulo 1), t ≡ t', t ≡ t", t ≡ t'"... O termo t' tem uma redução que, por hipótese, é o termo v, que está em Ts.

 

Detalhes do Produto

Livro Impresso
Book
Capítulos

Formato
PDF
Criptografado
Sim
SKU
BPP0000266721
ISBN
9788540700796
Tamanho do arquivo
9,2 MB
Impressão
Desabilitada
Cópia
Desabilitada
Vocalização de texto
Não
Formato
PDF
Criptografado
Sim
Impressão
Desabilitada
Cópia
Desabilitada
Vocalização de texto
Não
SKU
Em metadados
ISBN
Em metadados
Tamanho do arquivo
Em metadados