In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Formal specification (en)
- Formale Spezifikation (de)
- Especificación formal (es)
- Espezifikazio formala (informatika) (eu)
- 形式仕様記述 (ja)
- Especificação formal (pt)
- Формальная спецификация (ru)
- Формальна специфікація (uk)
|
| rdfs:comment
| - In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information. (en)
- Espezifikazio formala matematikak eskaintzen duen erabiliz, algoritmo baten zeregina dokumentatzean datza. Horretarako begizta edo egitura errekurtsiboen exekuzioen ondorioz lortutako emaitzen konputazio-egoerak lengoaia formalean zehazten dira, era horretan programak dokumentatzen dira. Dokumentazio horiek programen zeregina deskribatzean sarrerako datuen eta irteerako emaitzen arteko erlazioa adierazten dute.Espezifikazioa lehen mailako lengoaia logiko edo matematikoan idatzi ohi da, eguneroko hizkuntzek dituzten anbiguotasun eta zehaztasun gabeziak ekiditeko. Hala ere, espezifika daiteke lengoaia informalak diren eguneroko hizkuntzekin, aholkatzen ez den arren, horretarako oso ondo zehaztu behar baitira erabili beharreko terminoak, hizkuntzaren anbiguotasuna saihestuz. (eu)
- В информатике формальная спецификация — это математическое описание программной или аппаратной системы, которая может быть реализована в соответствии с этим описанием. Специфицируется, что должна делать система, но не то, как она должна это делать. Если существует спецификация системы, возможно применить методы формальной верификации, чтобы продемонстрировать, что система удовлетворяет (или будет удовлетворять) спецификации. Таким образом, можно проверить, будет ли конкретная спроектированная модель удовлетворять требованиям после реализации. Если верификация ПО исследует соответствие программы спецификации, то валидация исследует соответствие программы или спецификации требованиям пользователя. (ru)
- Eine formale Spezifikation ist die Beschreibung eines Computerprogramms mittels einer Notation, deren Semantik eindeutig definiert ist (einer sogenannten formalen Sprache). Ziel ist die formalisierte, präzise Beschreibung der zu lösenden Aufgabe in einem in sich konsistenten und geschlossenen Modell, um dieses weiterzuverarbeiten. Die Z-Notation ist ein Beispiel für eine formale Spezifikationssprache. Andere sind die Specification Language(VDM-SL) der Vienna Development Method und die Abstract Machine Notation (AMN) der . (de)
- Una especificación formal usa notación matemática para describir de manera precisa las propiedades que un sistema de información debe tener, sin preocuparse por la forma de obtener dichas propiedades. Describe lo que el sistema debe hacer sin decir cómo se va a hacer. (es)
- 形式仕様記述（けいしきしようきじゅつ、英: formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。 形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。 (ja)
- Uma especificação formal é uma descrição matemática de software ou de hardware que pode ser utilizada para desenvolver uma implementação dos mesmos. Descreve o que sistema deve fazer, e não (necessariamente) como o deve fazer. Dada uma especificação, é possível utilizar técnicas de verificação formal para demonstrar que o modelo de um sistema candidato está de acordo com a sua especificação. Isto tem a enorme vantagem de que sistemas candidatos incorrectos são detectados e podem ser revistos antes de se investir na sua implementação. Uma aproximação alternativa é utilizar passos de refinamento para transformar uma especificação num modelo completo, e por fim numa implementação concreta. (pt)
- Форма́льна специфіка́ція — математичний опис програмного забезпечення або обладнання, яке може бути використане для розробки реалізації. В ній описується, що має робити система, але не (обов'язково) вказується як. Маючи таку специфікацію, можна, використовуючи техніку формальної верифікації продемонструвати, що запропонований проєкт системи є правильним, по відношенню до специфікації. Такий підхід має перевагу в тому, що запропоновані невірні проєкти систем можуть бути переглянуті до того як буде зроблено основні витрати на власне саму реалізацію. Альтернативний підхід полягає в тому, аби, виконуючи кроки по специфікації, вірність яких можна довести, перетворити специфікацію на реалізацію, яка буде вірною через побудову. (uk)
|
| dcterms: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
| |
| date
| |
| url
| |
| has abstract
| - Eine formale Spezifikation ist die Beschreibung eines Computerprogramms mittels einer Notation, deren Semantik eindeutig definiert ist (einer sogenannten formalen Sprache). Ziel ist die formalisierte, präzise Beschreibung der zu lösenden Aufgabe in einem in sich konsistenten und geschlossenen Modell, um dieses weiterzuverarbeiten. Mit Hilfe von Zusatzwerkzeugen kann die Einhaltung der Regeln der formalen Sprache und die Integrität des Modells geprüft werden. Weitere Werkzeuge können eine Transformation des Modells in andere formale Sprachen bewirken, z. B. Programmiersprachen, die wiederum mit Compilern in auf Computern ausführbaren Maschinencode übersetzt werden können. Die Z-Notation ist ein Beispiel für eine formale Spezifikationssprache. Andere sind die Specification Language(VDM-SL) der Vienna Development Method und die Abstract Machine Notation (AMN) der . (de)
- Una especificación formal usa notación matemática para describir de manera precisa las propiedades que un sistema de información debe tener, sin preocuparse por la forma de obtener dichas propiedades. Describe lo que el sistema debe hacer sin decir cómo se va a hacer. Esta abstracción hace que las especificaciones formales sean útiles en el proceso de desarrollar un sistema, porque permiten responder preguntas acerca de lo que el sistema hace con confianza, sin la necesidad de tratar con una gran cantidad de información no relevante que se encuentra en el código de programa del sistema en un lenguaje de programación cualquiera, o especular sobre el significado de frases en un impreciso pseudocódigo. Un especificación formal pueden servir como un punto de referencia fiable para quienes se dedican a investigar sobre los requerimientos del cliente que solicita el sistema, o para que los desarrolladores de este sepan satisfacer esos requerimientos, y también para los que redactan manuales de instrucciones para el sistema. Debido a que es independiente del código del programa, las especificaciones formales de un sistema pueden ser elaboradas a principios de su desarrollo; y puede ser un medio valioso para promover un entendimiento común entre todos los interesados en el sistema. (es)
- In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information. (en)
- Espezifikazio formala matematikak eskaintzen duen erabiliz, algoritmo baten zeregina dokumentatzean datza. Horretarako begizta edo egitura errekurtsiboen exekuzioen ondorioz lortutako emaitzen konputazio-egoerak lengoaia formalean zehazten dira, era horretan programak dokumentatzen dira. Dokumentazio horiek programen zeregina deskribatzean sarrerako datuen eta irteerako emaitzen arteko erlazioa adierazten dute.Espezifikazioa lehen mailako lengoaia logiko edo matematikoan idatzi ohi da, eguneroko hizkuntzek dituzten anbiguotasun eta zehaztasun gabeziak ekiditeko. Hala ere, espezifika daiteke lengoaia informalak diren eguneroko hizkuntzekin, aholkatzen ez den arren, horretarako oso ondo zehaztu behar baitira erabili beharreko terminoak, hizkuntzaren anbiguotasuna saihestuz. (eu)
- 形式仕様記述（けいしきしようきじゅつ、英: formal specification）とは形式手法のひとつで、何らのシステムなどについて、その性質などの仕様を形式的に記述する手法や、そういった手法による仕様の記述である。 形式的な仕様を与えることにより、対象システムが仕様に照らして正しいかどうかを形式的に判定することが可能となる(形式的検証)。また、仕様策定の工程で仕様の不整合を検出することが可能となり、実装工程のような開発の後半での仕様不備発覚、それに伴う手戻り(多大なコストを要する場合が多い)を防ぐという利点がある。他の使われ方として、仕様から設計、設計から実装へと段階的に検証可能なステップを踏んで詳細化し、開発工程で不具合を作りこむのを防ぐ。 設計（や実装）の「正当性」はそれ自身だけで確認できないという点が重要である。正当性は与えられた仕様に照らして初めて検証可能であり、形式仕様記述が解決すべき問題を正しく記述できるかどうかは別の問題である。これもまた困難な問題であり、非形式的な実際の問題を抽象化された形式的仕様記述で正しく記述する問題に帰着する。そして、そのような抽象化は形式的証明が不可能である。しかし、仕様が表現することを期待されている特性に関わる定理を証明することによって仕様記述を検証することは可能である。もし検証結果が正しければ、それらの定理は仕様記述者の仕様記述および根底にある問題領域との関係への理解を深める。検証結果が正しくない場合、その仕様は元となっている問題領域を正しく反映しているとは言えないので、仕様記述者はさらに理解を深めて仕様記述を改訂することになるだろう。 (ja)
- Uma especificação formal é uma descrição matemática de software ou de hardware que pode ser utilizada para desenvolver uma implementação dos mesmos. Descreve o que sistema deve fazer, e não (necessariamente) como o deve fazer. Dada uma especificação, é possível utilizar técnicas de verificação formal para demonstrar que o modelo de um sistema candidato está de acordo com a sua especificação. Isto tem a enorme vantagem de que sistemas candidatos incorrectos são detectados e podem ser revistos antes de se investir na sua implementação. Uma aproximação alternativa é utilizar passos de refinamento para transformar uma especificação num modelo completo, e por fim numa implementação concreta. É importante notar que um modelo (ou implementação) nunca pode ser declarado "correcto" isoladamente, mas apenas "correcto no que diz respeito à sua especificação". Determinar se uma especificação formal descreve correctamente o problema a resolver, é um problema à parte. É também um problema de difícil resolução, uma vez que consiste em construir uma representação formal abstracta de um domínio de problema informal e concreto, e este passo de abstracção não é responsável nem suficiente para ser por si só uma prova formal. No entanto, é possível validar uma especificação provando teoremas relativos às propriedades que o sistema deve possuir. Se se verificarem correctos, estes teoremas reforçam a compreensão da especificação, e a sua relação com o domínio do problema. Se não, a especificação provavelmente necessita de ser alterada para melhor reflectir a compreensão do domínio de quem está envolvido na produção (e implementação) da especificação. (pt)
- Форма́льна специфіка́ція — математичний опис програмного забезпечення або обладнання, яке може бути використане для розробки реалізації. В ній описується, що має робити система, але не (обов'язково) вказується як. Маючи таку специфікацію, можна, використовуючи техніку формальної верифікації продемонструвати, що запропонований проєкт системи є правильним, по відношенню до специфікації. Такий підхід має перевагу в тому, що запропоновані невірні проєкти систем можуть бути переглянуті до того як буде зроблено основні витрати на власне саму реалізацію. Альтернативний підхід полягає в тому, аби, виконуючи кроки по специфікації, вірність яких можна довести, перетворити специфікацію на реалізацію, яка буде вірною через побудову. Важливо зазначити, що проєкт (або реалізацію) ніколи не можна вважати «вірним» окремо, але, лише «вірним по відношенню до вказаної специфікації». (uk)
- В информатике формальная спецификация — это математическое описание программной или аппаратной системы, которая может быть реализована в соответствии с этим описанием. Специфицируется, что должна делать система, но не то, как она должна это делать. Если существует спецификация системы, возможно применить методы формальной верификации, чтобы продемонстрировать, что система удовлетворяет (или будет удовлетворять) спецификации. Таким образом, можно проверить, будет ли конкретная спроектированная модель удовлетворять требованиям после реализации. Если верификация ПО исследует соответствие программы спецификации, то валидация исследует соответствие программы или спецификации требованиям пользователя. (ru)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
![[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)