In computer science, program derivation is the derivation of a program from its specification, by mathematical means. To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification. The program thus obtained is then correct by construction. Program and correctness proof are constructed together. Program derivation tries to remedy these shortcomings by The Bird-Meertens Formalism is an approach to program derivation.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Program derivation (en)
- プログラム導出 (ja)
|
| rdfs:comment
| - プログラム導出とは、計算機科学において数学的手段を用いて仕様からプログラムを導き出すことである。 プログラムを「導出」するとは、通常そのままでは実行不可能な形式的仕様を記述し、数学的に正しい規則を適用して実行可能なプログラムに変換することを意味する。このような手法で得られたプログラムは（最初の仕様にバグがない限り）構造的に正しいことが証明されている。 形式的検証の場合、最初にプログラムを書き、それが与えられた仕様に照らして正しいことの証明を与える。この際の問題は以下の通りである。
* 結果として出てくる証明は長くて複雑になる。
* そのプログラムがどのように開発されたかを示せない。まるで「帽子から出てきたうさぎ」のように見える。 プログラム導出はそのような欠点を次のようにして改善する。
* 適切な数学的記法を新たに開発して証明を短くする。
* 仕様を操作することでプログラムを発見する。 プログラム導出とほぼ同義の用語として、transformational programming、algorithmics、deductive programming などがある。 (ja)
- In computer science, program derivation is the derivation of a program from its specification, by mathematical means. To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification. The program thus obtained is then correct by construction. Program and correctness proof are constructed together. Program derivation tries to remedy these shortcomings by The Bird-Meertens Formalism is an approach to program derivation. (en)
|
| dct:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - In computer science, program derivation is the derivation of a program from its specification, by mathematical means. To derive a program means to write a formal specification, which is usually non-executable, and then apply mathematically correct rules in order to obtain an executable program satisfying that specification. The program thus obtained is then correct by construction. Program and correctness proof are constructed together. The approach usually taken in formal verification is to first write a program, and then provide a proof that it conforms to a given specification. The main problems with this are that
* the resulting proof is often long and cumbersome;
* no insight is given as to how the program was developed; it appears "like a rabbit out of a hat";
* should the program happen to be incorrect in some subtle way, the attempt to verify it is likely to be long and certain to be fruitless. Program derivation tries to remedy these shortcomings by
* keeping proofs shorter, by development of appropriate mathematical notations;
* making design decisions through formal manipulation of the specification. Terms that are roughly synonymous with program derivation are: transformational programming, algorithmics, deductive programming. The Bird-Meertens Formalism is an approach to program derivation. (en)
- プログラム導出とは、計算機科学において数学的手段を用いて仕様からプログラムを導き出すことである。 プログラムを「導出」するとは、通常そのままでは実行不可能な形式的仕様を記述し、数学的に正しい規則を適用して実行可能なプログラムに変換することを意味する。このような手法で得られたプログラムは（最初の仕様にバグがない限り）構造的に正しいことが証明されている。 形式的検証の場合、最初にプログラムを書き、それが与えられた仕様に照らして正しいことの証明を与える。この際の問題は以下の通りである。
* 結果として出てくる証明は長くて複雑になる。
* そのプログラムがどのように開発されたかを示せない。まるで「帽子から出てきたうさぎ」のように見える。 プログラム導出はそのような欠点を次のようにして改善する。
* 適切な数学的記法を新たに開発して証明を短くする。
* 仕様を操作することでプログラムを発見する。 プログラム導出とほぼ同義の用語として、transformational programming、algorithmics、deductive programming などがある。 (ja)
|
| gold:hypernym
| |
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)