Classificações finais

Época normal: Foram lançadas no livro de termos.

Época especial:

(*) Estes alunos devem entrar em contacto com o docente da disciplina.

Bibliografia

Bibliografia essencial

• J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Livro em preparação: os capítulos relevantes para esta disciplina são o segundo, o terceiro e o quarto .

Bibliografia complementar

• A. Cunha. Cálculo de Programas: notas teórico-práticas. Departamento de Informática, Universidade do Minho, 2005. Documento em preparação: (PDF).

• R. Bird and O. de Moor. Algebra of Programming. Series in Computer Science. Prentice-Hall International, 1997. C. A. R. Hoare, series editor.

• Graham Hutton. Programming in Haskell. Cambridge University Press, 2007

• P. Hudak. The Haskell School of Expression - Learning Functional Programming Through Multimedia. Cambridge University Press, 1st edition, 2000. ISBN 0-521-64408-9.

-- JoseNunoOliveira - 14 Feb 2012

-- JoseNunoOliveira - 13 Feb 2012

Horário de Atendimento

• Em qualquer altura: via correio electrónico pressionando aqui. Qualquer outro meio de contacto será considerado informal, não se sentindo a equipa docente vinculada a dar uma resposta em tempo útil.

• Durante o período de aulas: de acordo com o horário seguinte, sujeito a marcação verbal junto do respectivo docente:

• Essa marcação deve ser feita com um mínimo de uma semana de antecedência.

Atendimento electrónico (FAQs)

FAQ1 - Como mostro a igualdade entre (f . id) x (g + id).i1 e f x (g + id) . ( id x i1)?

R: O problema é a falta de uns parênteses: para f x (g + id) . ( id x i1) tipar bem é preciso colocar parênteses à esquerda da composição: (f x (g + id)) . ( id x i1). Depois é só aplicar a lei functor-x. NB: na nossa notação a composição tem prioridade sobre qualquer outro combinador.

FAQ2 - Gostaria de saber se a função (A x C + B x D) -- [pi2,pi2] --> C + D está bem tipada.

R: Para estar era preciso que as duas instâncias de pi2 tivessem o mesmo tipo de saída. Ora isso não acontece: tem-se A x C -- pi2 --> C num caso e B x D -- pi2 --> D no outro, ambos diferentes de C + D. Isto explica o que se deve fazer: escrever pi2 + pi2 em vez de [pi2,pi2].

FAQ3 - Como devo abordar a questão 6 do Teste de LEI do ano de 2009?.

R: O tipo From a é definido por data From a = First a | Next (From a) na questão 4.

Logo tem-se From a isomorfo a F(From a), para F X = a + X e F f = id + f. Tem-se ainda in = [First,Next] e

out(First a) = i1 a out(Next x) = i2 x

Para converter rev num hilo deste tipo teremos que encontar os seus dois genes divide e conquer tais que aux = conquer . (F aux) . divide. Pelo tipo _aux :: ([a], [a]) -> [a]: vê-se que os tipos têm de ser

divide : [a] x [a]->([a] x [a])

e

conquer : F [a] -> [a]

Das cláusulas

aux([],l) =l aux(h:t,l) = aux (t,h:l)

infere-se

divide([],l) = i1 l divide (h:t,l) = i2(t,h:l)

Como nada acontece após a chamada recursiva nessas mesmas cláusulas, ter-se-á

conquer = [id,id]

Para ver isto a funcionar implemente-se em Haskell:

data From a = First a | Next (From a) deriving Show

inF = either First Next

outF(First a) = i1 a

outF(Next x) = i2 x

cataF h = h . recF (cataF h) . outF

recF f = id -|- f

anaF g = inF . (recF (anaF g) ) . g

hyloF g h = cataF g . anaF h

divide([],l) = i1 l

divide (h:t,l) = i2(t,h:l)

conquer = either id id

Ver-se-á que, por exemplo,

hyloF conquer divide ([1,2,3],[4,5]) == aux([1,2,3],[4,5]) etc

FAQ4 - Tenho uma dúvida na última propriedade do exercício 2 (Ficha nr 4): pegando na primeira parte da igualdade e usando duas vezes a propriedade (53) do formulário, obtenho [[a,b].p?,[c,d].p?].p? Posso neste momento posso usar a propriedade (20), absorçao-+? Assim obtinha [[a,b],[c,d]].(p?+p?).p? de onde prossigo usando (3) da mesma ficha.

R: Claro que sim, esse é o caminho a seguir. De um modo geral, sempre que tiver uma alternativa de (quaisquer) composições a lei é aplicável, dando uma composição de uma alternativa com uma soma.

FAQ5 - Gostaria de perceber melhor a razão para haver uma notação funcional com variáveis ("pointfree") e outra sem elas ("pointwise") e qual se deve escolher e em que circunstâncias.

Sem variáveis os programas ficam reduzidos a expressões algébricas sobre as quais se pode raciocinar usando o Cálculo de Programas. Após os cálculos (eg. conversão da função de Fibonacci - recursiva e ineficiente -- num ciclo -- não recursivo, eficiente ) converte-se o resultado final de novo para Haskell com variáveis e... "entrega-se ao cliente". Se tentar fazer o mesmo sempre com variáveis os cálculos terão que usar provas por indução matemática e serão mais longos e (para muitos) difíceis de perceber.

-- JoseNunoOliveira - Página criada em 14 Feb 2012

Material Pedagógico

Fichas das aulas práticas

• Ficha 1
• Ficha 2
• Ficha 3
• Ficha 4
• Ficha 5
• Ficha 6
• Ficha 7
• Ficha 8
• Ficha 9
• Ficha 10
• Ficha 11

Notas pedagógicas

• What is the meaning of curry / uncurry?

Transparentes

• Transparentes mostrados nas teóricas da segunda semana de aulas: Towards Formal Software Development in VS.NET (slides 20 a 33)

Bibliotecas de Software

• demos.hs - contendo material auxiliar para a visualização em HTML da estrutura de dados virtual (intermédia) dos hilomorfismos qSort, hanoi, mSort etc das bibliotecas BTree.hs e LTree.hs. Experimentar qSort_vtree [6,3,9,1,7,18] e hanoi_vtree (True, 7), por exemplo. Encontrar-se-á a visualização no ficheiro _.html da directoria corrente.
• LTree.hs - biblioteca contendo os cata/ana/hilomorfismos do tipo de dados árvores binárias de folhas - LTree a = Leaf a | Split (LTree a, LTree a) e aplicações suas (e.g. duplo factorial, `merge-sort', Fibonacci etc).
• BTree.hs - biblioteca contendo os cata/ana/hilomorfismos do tipo de dados árvores binárias - data BTree a = Empty | Node(a, (BTree a, BTree a)), e aplicações suas (e.g. torres de Hanói, `quick-sort', etc).
• Exp.hs - biblioteca auxiliar a demos.hs.
• List.hs - biblioteca geral para listas em Haskell, contendo a respectiva bateria de combinadores ana+cata+hilo e exemplos de utilização, que incluem os dados nas aulas.
• Nat.hs - biblioteca de naturais (ciclos-for, etc).
• Cp.hs - contendo os combinadores de base da notação adoptada, e.g. split, ><, -|- etc.

Enunciados de provas de avaliação

Outro material

• Formulário

-- JoseNunoOliveira - 14 Feb 2012

Regime de Avaliação

Os alunos devem escolher um dos seguintes métodos de avaliação (época normal):

Método A:

• 2 Fichas individuais (3 questões cada, sem consulta) a realizar nas aulas TP: 12 valores (total de 6 questões), com nota mínima de 8 valores
• Prova individual escrita (sem consulta e só para alunos com nota mínima): 8 valores - a realizar no dia 18-Junho, conforme consta do calendário da disciplina.
• A opção pelo Método A faz-se no momento de inscrição e é uma opção individual e irreversível durante o semestre.

Método B:

• Prova individual escrita (sem consulta): 20 valores, com nota mínima de 10 valores - a realizar no dia 18-Junho, conforme consta do calendário da disciplina.

IMPORTANTE: Condições de frequência/avaliação:

• Alunos de 1ª inscrição: podem escolher entre os métodos de A ou B.
• Outros alunos: quem frequentou o método de avaliação A em (quaisquer) anos anteriores só pode escolher o método B. (A sua inscrição no método A será liminarmente rejeitada.)

-- jno - 13 Feb 2012

50 Recent Changes in TWiki Web retrieved at 16:39 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

Benvindo a Cálculo de Programas

Bem vindo à página da edição de 2011/12 da disciplina de Cálculo de Programas. O meu nome é José Nuno Oliveira e sou o responsável por esta disciplina, que conta com uma equipa de docentes altamente qualificados na investigação e ensino de métodos que, como os que se leccionam nesta disciplina, estão na base da abordagem científica ao desenvolvimento de software. Todos fazemos parte do Laboratório HASLab (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais de programação desde há mais de 25 anos.

A palavra "programa" vem do grego "programma", uma derivação de "prographein" = "pro" (antes) + "graphein" (escrever). Isto sugere que alguém que programa deve pensar antes no que vai fazer.

Cada vez mais, a indústria pede às universidades que ensinem a programar a sério, isto é, de forma reflectida, capaz de evitar erros de programação. Para isso, é preciso introduzir a noção de cálculo em programação, isto é, uma disciplina que nos ajude a pensar os programas, raciocinar sobre eles e obter versões eficientes sem que a sua correcção fique comprometida.

A Universidade do Minho tem uma longa tradição neste tipo de ensino. Cálculo de Programas é a cadeira que, nas licenciaturas de Eng. Informática e Ciências da Computação, ensina tais competências. Mais do que tecnologia ensina-se método, que é afinal aquilo que a maioria dos programadores não tem de facto.

Resultados da Aprendizagem

• Construção de programas: escrever programas funcionais de forma composicional, com recurso a combinadores algébricos.

• Transformação de programas: recurso à algebra da programação para se obterem programas mais eficientes sem comprometer as sua correcção.

• Análise e compreensão de programas: recurso à factorização em pares "fold" + "unfold" (hilomorfismos) como forma de se perceber a arquitectura dos algoritmos e sua catalogação.

• Síntese de programas: cálculo de ciclos-for a partir de definições indutivas da matemática.

• Programação funcional avançada: construir e raciocinar sobre programas funcionais com efeitos sob a forma de mónades.

Página principal

Entrar aqui.

Education/CP1112 Web Preferences

The following settings are web preferences of the Education.CP1112 web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

Web Preferences Settings

These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.

Natural Skin configuration

• Set SKIN=nat

• Set SKINSTYLE = Plain
• Set STYLEBORDER = thin
• Set STYLEBUTTONS = off
• Set STYLESIDEBAR = left
• Set STYLEVARIATION = none
• Set STYLESEARCHBOX = off

• Set PAGETITLE= Cálculo de Programas

• Set NATWEBLOGO = Cálculo de Programas

• Set WEBCOPYRIGHT = Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

• List of topics of the Education/CP1112 web:
  • #Set WEBTOPICLIST = Changes | Index | Search | Go

• Web-specific background color: (Pick a lighter one of the StandardColors).
  • Set WEBBGCOLOR = #D0D0D0
  • Note: This setting is automatically configured when you create a web

• Image, URL and alternate tooltip text of web's logo.
  Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.

• Set WEBLOGOURL = WebHome
• Set WEBLOGOIMG =
• Set WEBLOGOALT = Cálculo de Programas

• List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/CP1112.Topic links.
  Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
  
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = Cálculo de Programas
  • Set SITEMAPUSETO = Licenciaturas em Engenharia Informática e Ciências da Computação
  • Note: Above settings are automatically configured when you create a web

• Exclude web from a web="all" search: (Set to on for hidden webs).
  • Set NOSEARCHALL =
  • Note: This setting is automatically configured when you create a web

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Education/CP1112 web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW =
  • #Set DENYWEBCHANGE =
  • #Set ALLOWWEBCHANGE = JoseNunoOliveira
  • #Set DENYWEBRENAME =
  • #Set ALLOWWEBRENAME = JoseNunoOliveira

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = TWikiAdminGroup
  • Set ALLOWTOPICRENAME = TWikiAdminGroup

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Web Search

Search: \.*

Tópicos

• Apresentação
• Docentes
• Contacto
• BB (1112.8204N5)
• Página pública
• Alunos
• Regime de Avaliação
• Horário
• Atendimento
• Sumários
• Programa
• Material
• Bibliografia

Avisos