Ano lectivo de 1995/96
O presente texto descreve a proposta de trabalho laboratorial (opcional) da disciplina Métodos Formais de Programação II da Licenciatura em Matemática e Ciências da Computação , na sua edição de 1995/96.
O que se pretende neste trabalho é que os alunos adquiram prática laboratorial na área da ``prototipagem rápida'' em Métodos Formais de especificação e desenvolvimento de aplicações.
O tema do trabalho é, para além disso, uma simples motivação para o estudo das Bases de Dados Temporais .
A gestão pedagógica na Universidade do Minho é, nos dias de hoje, uma actividade frustrante: a massa discente é muita, a informação (sumários, fichas de avaliação, fichas estatísticas etc. ) está dispersa, circula redundantemente pelos vários níveis da instituição e, quando está em suporte informático, as fontes de informação não estão interligadas e, mesmo que o estivessem, as diferentes plataformas, formatos etc. não dialogam entre si com facilidade. Mais ainda, um dos principais destinatários dessa informação --- o aluno --- tem acesso deficiente à informação que lhe diz respeito.
A necessidade de avaliar o funcionamento da Licenciatura em Matemática e Ciências da Computação durante o ano lectivo de 94/95 levou o Director de Curso a especificar formalmente, e prototipar (em CAMILA ), um modelo da informação necessária para produzir o relatório de auto-avaliação. Presentemente, esse protótipo exporta informação para LaTeX , mas também o poderá vir a fazer para HTML ou RTF /WORD.
Verifica-se que o modelo até agora desenvolvido tem potencialidade para ser estendido a ponto de vir ser o embrião de um sistema de informação pedagógica sobre o funcionamento de todos os cursos da U.Minho , articulável com um ``mirror'' da base de dados dos Serviços Académicos e globalmente acessível via INTERNET.
O que se pretende neste trabalho é estender o modelo acima referido por forma a:
O modelo em causa é listado no fim deste texto, no Anexo I, em que se transcreve directamente a fonte CAMILA (apenas omitindo a funcionalidade). No Anexo II dá-se, como configuração inicial do sistema, ainda atemporal, a ``fotografia'' da Licenciatura em Matemática e Ciências da Computação no ano lectivo de 94/95.
Na secção que se segue descreve-se sumariamente o modelo formal dos dados, por forma a poderem ser entendidos os requisitos que se lhe seguirão.
A base de dados correntemente prototipada tem a estrutura seguinte, referente a um único ano lectivo de um só curso:
Bd :: P: PlanoEstudos
D: Docentes
Dp: Depts
A: AriCient;
Quer dizer,
regista-se o plano de estudos do curso, os docentes nele envolvidos,
os departamentos que asseguram o curso e as suas áreas centíficas.
O plano de estudos é um conjunto de disciplinas,
PlanoEstudos = Disciplina-set;Uma disciplina pode ser obrigatória, opcional ou o estágio:
Disciplina = Obriga | Opcional | Estagio;A informação de uma disciplina obrigatória,
Obriga :: A: Ano
AL: ALect
AC: ACien
N: Nome
R: Regime
E: Esc
D: EquDoc
Al: Alunos;
é praticamente a mesma de uma disciplina opcional,
Opcional :: A: Ano
AL: ALect
AC: ACien-set
N: Nome
R: Regime
O: Opcao-set;
a principal diferença residindo no facto de
as segundas dividirem os alunos inscritos por uma ou mais opções,
Opcao :: AC: ACien
N: Nome
E: Esc
D: EquDoc
Al: Alunos;
cada uma com nome próprio e equipa docente distinta.
Quanto a áreas científicas, uma disciplina opcional pode admitir
opções de mais do que uma, enquanto que uma disciplina obrigatória
tem sempre uma e uma só área científica.
Toda a disciplina tem um regime, anual ou semestral, e uma escolaridade,
Esc = STR -> InfEsc;onde, para cada tipo de aula, se indica o número de horas semanais, o número de turmas, o número total de horas previstas e o número total de horas efectivamente leccionadas:
InfEsc :: H:INT T:INT HLP:INT HLE:INT;
A informação referente ao aproveitamento dos alunos,
Alunos :: In:INT Av:INT Ap:INT;indica o número de inscritos, o de avaliados e o de aprovados (esta informação fica disponível no final de cada ano lectivo).
Quanto às esquipas docentes,
EquDoc :: R: IdDoc
O: IdDoc-set;
elas constam sempre de um docente responsável e de um conjunto
(possivelmente vazio) de docentes auxiliares.
Cada docente é identificado por um código ( IdDoc) que é
chave na estruira
Docentes = IdDoc -> Docente;de Bd, onde
Docente :: N: Nome C: Cat D: Dep G:Grau;contém a informação habitual (nome, categoria, departamento e grau académico).
Como requisito opcional, o grupo poderá embeber o seu protótipo em C e construir um browser em HTML que chame esse protótipo (ver manuais disponíveis na documentação CAMILA ).
Duas semanas antes do lançamento das notas no livro de termos, ie. 17 de Julho de 1996.
TYPE
Bd :: P: PlanoEstudos
D: Docentes
Dp: Depts
A: AriCient;
Depts = Dep -> InfDep;
InfDep :: N: Nome;
PlanoEstudos = Disciplina-set;
AriCient = ACien -> Nome;
Docentes = IdDoc -> Docente;
Docente :: N: Nome C: Cat D: Dep G:Grau;
AnoLec = INT;
Disciplina = Obriga | Opcional | Estagio;
Obriga :: A: Ano
AL: ALect
AC: ACien
N: Nome
R: Regime
E: Esc
D: EquDoc
Al: Alunos;
Opcional :: A: Ano
AL: ALect
AC: ACien-set
N: Nome
R: Regime
O: Opcao-set;
Opcao :: AC: ACien
N: Nome
E: Esc
D: EquDoc
Al: Alunos;
Estagio :: A: Ano
AL: ALect
R: Regime
Al: Alunos;
EquDoc :: R: IdDoc
O: IdDoc-set;
Alunos :: In:INT Av:INT Ap:INT;
Esc = STR -> InfEsc;
InfEsc :: H:INT T:INT HLP:INT HLE:INT;
IdDoc = STR;
Grau = STR;
Cat = STR;
Dep = STR;
Ano = INT;
ALect = INT;
ACien = STR;
Nome = STR;
Regime = STR;
STRs = STR-list;
ENDTYPE
FUNC INIT():SYM
RETURN
bd <- Bd(
{
Obriga(1,9495,"alg",
;7001A6
"'Algebra Linear e Geometria Anal'itica","A",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("mmargseq",{"cmendes"}),
Alunos(164,78,18)
),
Obriga(1,9495,"anl",
;7001A5
"An'alise I","A",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("estrada",{"elrv","jmo"}),
Alunos(161,108,43)
),
Obriga(1,9495,"cc",
;700143
"Algor'itmos e Estruturas de Dados","A",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(1,0,0,0),
"P"-> InfEsc(2,0,0,0)],
EquDoc("fmm",{"af","anr"}),
Alunos(119,84,47)
),
Obriga(1,9495,"cc",
;700144
"Linguagens de Programa,c~ao","A",
["T"-> InfEsc(2,0,0,0),
"P"-> InfEsc(3,0,0,0)],
EquDoc("fmm",{"jgr","jas"}),
Alunos(122,90,49)
),
;
Obriga(2,9495,"anl",
;7003A1
"An'alise II","A",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("vilar",{"amaral"}),
Alunos(85,13,1)
),
Obriga(2,9495,"ann",
;7003A2
"An'alise Num'erica","A",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("joana",{"rseverino"}),
Alunos(52,36,25)
),
Obriga(2,9495,"anl",
;7004N1
"Matem'atica Discreta","2",
["T"-> InfEsc(2,1,0,0),
"TP"-> InfEsc(2,2,0,0)],
EquDoc("psmith",{"fpinto","lpinto"}),
Alunos(58,47,39)
),
Obriga(2,9495,"cc",
;7003A3
"Programa,c~ao Formal","A",
["T"-> InfEsc(2,0,0,0),
"P"-> InfEsc(2,0,0,0)],
EquDoc("jmv",{"mjf"}),
Alunos(71,50,40)
),
Obriga(2,9495,"cc",
;7003A4
"Teoria das Linguagens e da Compila,c~ao","A",
["T"-> InfEsc(2,0,0,0),
"P"-> InfEsc(2,0,0,0)],
EquDoc("prh",{"jj"}),
Alunos(59,21,19)
),
Obriga(2,9495,"ec",
; 7003N1
"Arquitectura de Computadores","1",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(2,0,0,0)],
EquDoc("aproenca",{"hsantos"}),
Alunos(92,51,18)
),
;
Obriga(3,9495,"ann",
;7006N1
"Complementos de An'alise Num'erica","2",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(2,0,0,0)],
EquDoc("r_ralha",{}),
Alunos(48,41,31)
),
Obriga(3,9495,"alg",
;7005A1
"'Algebra","A",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("psmith",{"pmartins"}),
Alunos(116,77,52)
),
Obriga(3,9495,"alg",
;7005N1
"L'ogica","1",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(2,0,0,0)],
EquDoc("assis",{"amaral","lantunes"}),
Alunos(94,77,28)
),
Obriga(3,9495,"ann",
;7005N3
"Probablidades e Estat'istica","1",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("atha",{"apa"}),
Alunos(66,43,22)
),
Obriga(3,9495,"ann",
;7006N3
"Estat'istica Aplicada","2",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("pno",{}),
Alunos(54,37,29)
),
Obriga(3,9495,"cc",
;7005A3
"Sistemas Operativos","A",
["T"-> InfEsc(3,0,0,0),
"P"-> InfEsc(3,0,0,0)],
EquDoc("fsm",{"rco","vff"}),
Alunos(91,49,43)
),
Obriga(3,9495,"ci",
;7005A4
"Bases de Conhecimento e Sistemas Inteligentes","A",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("jneves",{"jmac","pjon"}),
Alunos(37,33,32)
),
;
Obriga(4,9495,"alg",
;7007A1
"'Algebra Universal","A",
["T"-> InfEsc(2,0,0,0),
"TP"-> InfEsc(2,0,0,0)],
EquDoc("assis",{}),
Alunos(77,29,17)
),
Obriga(4,9495,"ann",
;7007A2
"Investiga,c~ao Operacional","A",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(3,0,0,0)],
EquDoc("agr",{"telhada","gui"}),
Alunos(59,32,23)
),
Obriga(4,9495,"cc",
;7007A3
"Compiladores","A",
["T"-> InfEsc(2,1,0,0),
"P"-> InfEsc(3,1,0,0)],
EquDoc("prh",{}),
Alunos(44,40,39)
),
Obriga(4,9495,"cc",
;7007A4
"Especifica,c~ao e Sem^antica","A",
["T"-> InfEsc(2,1,0,0),
"P"-> InfEsc(3,1,0,0)],
EquDoc("jno",{"omp"}),
Alunos(46,41,28)
),
Obriga(4,9495,"ci",
;7007A5
"Processamento de Dados","A",
["T"-> InfEsc(3,0,0,0),
"P"-> InfEsc(2,0,0,0)],
EquDoc("j_nuno",{}),
Alunos(40,38,36)
),
;
Opcional(5,9495,{"cc","ci"},
;7009N7
"Op,c~ao I","1",
{ Opcao("cc","Complementos de Especifica,c~ao e Sem^antica",
["T"-> InfEsc(2,0,0,0),
"P"-> InfEsc(2,0,0,0)],
EquDoc("jno",{"omp"}),
Alunos(15,15,15)
),
;7009N4
Opcao("cc","Processos, Objectos e Comunica,c~ao",
["T"-> InfEsc(2,0,0,0),
"P"-> InfEsc(2,0,0,0)],
EquDoc("pinj",{}),
Alunos(15,15,11)
)
}),
Opcional(5,9495,{"cc","ci"},
;7009N9
"Op,c~ao II","1",
{ Opcao("cc","Prototipagem R'apida de Software",
["TP"-> InfEsc(1,0,0,0),
"P"-> InfEsc(5,0,0,0)],
EquDoc("fmm",{}),
Alunos(15,15,15)
),
;7009N8
Opcao("cc","L'ogica e Reescrita",
["TP"-> InfEsc(1,0,0,0),
"P"-> InfEsc(5,0,0,0)],
EquDoc("mjf",{}),
Alunos(14,14,12)
)
}),
Obriga(5,9495,"ec",
;7009N3
"Sistemas de Microcomputadores","1",
["T"-> InfEsc(3,0,0,0),
"P"-> InfEsc(4,0,0,0)],
EquDoc("aproenca",{"psantos"}),
Alunos(30,24,14)
),
Obriga(5,9495,"ci",
;7009A1
"An'alise Inform'atica","1",
["T"-> InfEsc(3,0,0,0),
"TP"-> InfEsc(4,0,0,0)],
EquDoc("maribel",{}),
Alunos(29,23,23)
),
Estagio(5,9495,"2",
Alunos(0,0,0)
)
},
[
"miguel" -> Docente("Jo~ao Miguel L. Fernandes","Assis","DI","M"),
;
"aproenca" -> Docente("Alberto Jos'e C. Proen,ca","P.Ass","DI","D"),
"jmv" -> Docente("Jos'e Manuel Esgalhado Valen,ca","P.Cat","DI","D"),
"r_ralha" -> Docente("Rui Manuel da S. Ralha","P.Aux","DM","D"),
"estrada" -> Docente("Maria Fernanda Estrada","P.Aux","DM","D"),
"elrv" -> Docente("Estelita Gra,ca R. Vaz","P.Ass","DM","D"),
"joana" -> Docente("Maria Joana E. Soares","P.Ass","DM","D"),
"vilar" -> Docente("Carlos Alberto da S. Vilar","P.Aux","DM","D"),
"rseverino" -> Docente("Ricardo Jos'e M. Severino","Assis","DM","M"),
"jneves" -> Docente("Jos'e Carlos Maia Neves","P.Ass","DI","D"),
"gui" -> Docente("Guilherme Pereira","Assis","DPS","M"),
"telhada" -> Docente("Jos'e Manuel H. Telhada","Assis","DPS","M"),
"pno" -> Docente("Pedro Nuno P. de Oliveira","P.Aux","DPS","D"),
"fsm" -> Docente("Francisco Coelho S. de Moura","P.Ass","DI","D"),
"jno" -> Docente("Jos'e Nuno Fonseca de Oliveira","P.Ass","DI","D"),
"mjf" -> Docente("Maria Jo~ao Gomes Frade","Assis","DI","M"),
"psantos" -> Docente("Lu'is Paulo P. dos Santos","Assis","DI","M"),
"jmac" -> Docente("Jos'e Manuel Ferreira Machado","Assis","DI","M"),
"amaral" -> Docente("Carlos Manuel S.C. Amaral","A.Est","DM","L"),
"pmartins" -> Docente("Maria Paula F. Martins","Assis","DM","M"),
"jmo" -> Docente("Jos'e Manuel Oliveira","A.Est","DM","L"),
"fpinto" -> Docente("Maria Fernanda Alves Pinto","Ass.C","DM","M"),
"lpinto" -> Docente("Lu'is Filipe Ribeiro Pinto","A.Est","DM","L"),
"cmendes" -> Docente("Carla Albertina Mendes","Assis","DM","M"),
"lantunes" -> Docente("Lu'is Filipe C. Antunes","A.Est","DM","L"),
"j_nuno" -> Docente("Jo~ao Nuno Oliveira","A.Est","DI","L"),
"anr" -> Docente("Ant'onio Nestor Ribeiro","A.Est","DI","L"),
"af" -> Docente("Ant'onio Ramires Fernandes","A.Est","DI","M"),
"maribel" -> Docente("Maribel Yasmina C. Alves","A.Est","DI","L"),
"vff" -> Docente("V'itor Francisco G. da Fonte","A.Est","DI","L"),
"hsantos" -> Docente("Henrique Manuel Santos","Assis","DI","M"),
"rco" -> Docente("Rui Carlos Mendes Oliveira","Assis","DI","M"),
"omp" -> Docente("Olga Maria Pacheco","Assis","DI","M"),
"jj" -> Docente("Jos'e Jo~ao G.D. Almeida","Assis","DI","M"),
"jas" -> Docente("Jos'e Alexandre Saraiva","Assis","DI","M"),
"jgr" -> Docente("Jorge Gustavo Rocha","Assis","DI","M"),
"fmm" -> Docente("Fernando M'ario J. Martins","Assis","DI","D"),
"pjon" -> Docente("Paulo Jorge F.O. Novais","Assis","DI","M"),
"pinj" -> Docente("Jos'e Eduardo Pina Miranda","Assis","DI","M"),
"prh" -> Docente("Pedro Rangel Henriques","P.Aux","DI","D"),
"apa" -> Docente("Ana Paula Amorim","Assis","DM","M"),
"atha" -> Docente("Maria Em'ilia F. Queiroz de Athayde","P.Aux","DM","D"),
"assis" -> Docente("Jos'e Assis Ribeiro de Azevedo","P.Ass","DM","D"),
"agr" -> Docente("Ant'onio Guimar~aes Rodrigues","P.Ass","DPS","D"),
"psmith" -> Docente("Maria Paula Marques Smith","P.Ass","DM","D"),
"mmargseq" -> Docente("Maria Margarida R. Sequeira","P.Aux","DM","D")
],
[
"DM" -> InfDep("Departamento de Matem'atica"),
"DI" -> InfDep("Departamento de Inform'atica"),
"DPS" -> InfDep("Departamento de Produ,c~ao e Sistemas")
],
[
"alg" -> "'Algebra e Teoria Alg'ebrica da Computa,c~ao",
"anl" -> "An\'alise",
"ann" -> "An'alise Num'erica, Estat'istica e Investiga,c~ao Operacional",
"cc" -> "Ci^encias da Computa,c~ao",
"ci" -> "Ci^encias da Informa,c~ao",
"ec" -> "Engenharia de Computadores",
"" -> "Est'agio"
]);
A temporalização de um modelo de informação pode ser vista como uma operação de ``desdobramento no tempo'' das chaves de acesso à informação. Estas passam a dar acesso não só à ``fotografia actual'' da informação mas à própria vida (passada ou prevista para o futuro) dessa informação.
Neste trabalho só nos preocuparemos com a temporalização da estrutura A -> B, ie, de funções finitas. Mas note-se que ficam também ficam cobertas as estruturas A-set, pois A-set é isomorfo a A -> 1. Seja então A -> B uma entidade atemporal. A sua temporalização corresponde a estender esse modelo a
A -> (T-> B)+
onde T é a espécie de dados tempo que for relevante escolher (eg. dias, anos lectivos) e o + designa um invariante que força finções finitas não-vazias. Quer dizer, cada chave A dá acesso, para cada t no domínio de (T-> B)+, ao valor de B que entrou em vigor na data t (ou entrará em vigor na data t, caso t seja superior ao tempo actual).
Ora A -> (T-> B)+ é isomorfo a (A x T)-> B . Obtém-se assim o correspondente modelo temporal. Para A-set, não é difícil ver que o correspondente modelo temporal fica (A x T)-set. Suponhamos agora que A é chave estrangeira noutra função finita, por exemplo,
C -> (A x D)
que, temporalizada, fica
(C x T) -> (A x D)
Para que este modelo tenha a semântica esperada há que garantir o seguinte invariante:
Assim se garantirá a extensão temporal da integridade referencial do modelo formal de dados. Agora, supondo que o conjunto de todos os t' nas condições do invariante anterior não é singular, qual é aquele a que f[<c,t>] se está de facto a referir? A funcionalidade deverá garantir que é o respectivo supremo ( T deverá ter uma ordem total associada). Em suma, só se pode referir o passado mas subentende-se que se está a referir sempre o passado mais recente.
Note-se que a temporalidade pode e deve introduzir-se gradualmente, espécie a espécie, havendo espécies cuja temporalização não se justifica. No modelo de dados apresentado, as espécies Docentes e PlanoEstudos são aquelas cuja temporalização mais interessa, por serem aquelas que mais variam no tempo. A recente re-estruturação da Licenciatura em Matemática e Ciências da Computação é disso um bom exemplo: só uma base de dados temporal poderá fazer coexistir o plano antigo com o plano novo!