notação matemática de conceitos de programação
-
06-07-2019 - |
Pergunta
Existem muitos métodos para representar estrutura de um programa (como classe UML diagramas etc.). Estou interessado se existe uma convenção que descreve os programas de uma forma rigorosa, matemática. Estou especialmente interessado no uso de notação matemática para esta finalidade.
Solução
Eu sei que Z Notação tem sido usado em certa medida, a verificação formal de software, tais como o projeto Tokeneer .
Outras dicas
Sim, existe, Floyd -Hoare Logic .
Há um monte de forma, mas eu acho que a maioria deles são inconvenientes para expressar a estrutura já que a estrutura muitas vezes não é expressável em conceitos matemáticos padrão. A principal exceção é de linguagens de programação curso funcionais. Pense em dobras (catamorphisme), grupos de álgebra etc.
Para programação imperativa Eu sei da existência de Z, que usa (puros e estendida) a teoria dos conjuntos lambda cálculo e (primeira ordem) lógica de predicados. No entanto, eu não acho que é muito conveniente. A única vantagem de usar a matemática para expressar estrutura é o fato de que você pode provar coisas sobre ele. Mas se você quiser fazer isso, dê uma olhada JML, Spec # ou Eiffel.
depende do que você está tentando realizar, mas indo por este caminho com linguagens específicas pode trazer-lhe problemas.
Por exemplo, veja o círculo-elipse discussão em C ++ FAQ Lite.
Este livro aplica-se o método dedutivo a programação por programas de afiliação com o matemático abstrato teorias que lhes permitam trabalhar. [...]
Eu acredito que Elementos de Programação por Alexander Stepanov e Paul McJones, é muito parecido com o que você é procurando.
Um conceito é uma descrição requisitos de um ou mais tipos declarou em termos da existência e Propriedades de procedimentos, tipo atributos, e as funções do tipo definido sobre os tipos.
Z, que já foi mencionado, é muito bonito o que você descreve. Existem algumas variantes do mesmo para a modelagem orientada a objetos, mas acho que você pode ficar muito longe com "padrão Z de" esquemas se você deseja classes de modelo.
Há também Alloy , que é mais recente e inspirado por Z. Sua notação é talvez um pouco mais perto do objeto -orientação. Também é analisável, ou seja, você pode conferir os modelos criados se cumprem certas condições, mas não pode provar que as propriedades segurar, apenas tentar refutar dentro de um escopo finito.
O artigo confiável Software by Design é uma boa introdução para Alloy e sua laia, juntamente com uma mesa de ferramentas similares disponíveis.
Você está procurando programação funcional. Existem várias linguagens de programação funcional, e eles são tudo baseado em uma teoria matemática fundamentais chamado Lambda calculus . Programas escritos em uma linguagem de programação funcional, como LISP são uma representação matemática de si mesmos. ; -)
Há uma linguagem matemática que descreve realmente um programa ou melhor, de operações. Você pega o estado inicial e, em seguida, transformar este estado até chegar ao estado de destino desejado. As transformações produzir o código de programa que deve ser executado.
Veja a href="http://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow noreferrer"> artigo .
A idéia básica é que, para cada função (não importa se você colocar isso em uma classe ou em uma função de estilo antigo), você tem um pré e um pós-condição. Por exemplo, a pré-condição pode ser que você tenha um array que tem elementos >= 0
. a pós-condição é de que cada elemento de [i] mosto por <= elemento [j] para todos os i <= j.
A descrição habitual seria "a função ordena a matriz". Mas os termos matemáticos permitem transformar a entrada (que deve corresponder a pré-condição) para a saída (que deve corresponder a pós-condição).
É um pouco complicado de usar, especialmente para programas mais complexos, mas alguns dos exemplos são bastante impressionantes. Muitas vezes, você obtém o código realmente compacto como o resultado que parece bastante complexo, mas funciona na primeira tentativa.
Eu gostaria de sugerir Álgebra de programação . É uma abordagem calculacional de programas, usando Álgebra Relacional , e Conexões de Galois .
Se você tem mais interesse sobre este tema, você pode encontrar um trabalho incrível, aqui , por Shin-Cheng Mu, e José Nuno Oliveira ( lâminas ).
Usando relacional Álgebra e Lógica de Primeira Ordem, também tem uma sinergia agradável com Alloy , programação funcional e programação por contrato (facilmente aplicada a Programação Orientada a objetos).