Formal specification (original) (raw)

About DBpedia

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.

Property Value
dbo: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)
dbo:wikiPageExternalLink http://kuro5hin.org/story/2005/7/29/04553/9714 https://web.archive.org/web/20051021002908/http:/www.kuro5hin.org/story/2005/7/29/04553/9714
dbo:wikiPageID 2567707 (xsd:integer)
dbo:wikiPageLength 11735 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID 1097140681 (xsd:integer)
dbo:wikiPageWikiLink dbr:Algebraic_specification dbr:Requirements_analysis dbr:OBJ_(programming_language) dbr:Correctness_(computer_science) dbr:Theorem dbc:Formal_specification dbr:Communicating_sequential_processes dbr:Computer_science dbr:Petri_net dbr:Specification_(technical_standard) dbr:Specification_language dbr:Software_engineering dbc:Formal_specification_languages dbr:Web_services dbr:Domain_(software_engineering) dbr:Language_Of_Temporal_Ordering_Specification dbr:Larch_family dbr:Agile_software_development dbr:Formal_verification dbr:Formal_methods dbr:Formal_specification dbr:Quality_of_service dbc:Formal_methods dbr:TLA+ dbr:Z_notation dbr:Model-based_specification dbr:Divide_and_conquer_algorithm dbr:B-Method dbr:Software_testing dbr:Separation_of_concerns dbr:Verification_and_validation dbr:Vienna_Development_Method dbr:Implementation dbr:Specification dbr:Program_refinement dbr:Abstract_Machine_Notation dbr:Paisley_(programming_language)
dbp:date 2005-10-21 (xsd:date)
dbp:url https://web.archive.org/web/20051021002908/http:/www.kuro5hin.org/story/2005/7/29/04553/9714
dbp:wikiPageUsesTemplate dbt:Commonscat dbt:Reflist dbt:Short_description dbt:Webarchive
dcterms:subject dbc:Formal_specification dbc:Formal_specification_languages dbc:Formal_methods
rdf:type yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Communication100033020 yago:Know-how105616786 yago:Language106282651 yago:Method105660268 yago:PsychologicalFeature100023100 yago:WikicatFormalLanguages yago:WikicatFormalMethods yago:WikicatFormalSpecificationLanguages
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)
rdfs:label Formal specification (en) Formale Spezifikation (de) Especificación formal (es) Espezifikazio formala (informatika) (eu) 形式仕様記述 (ja) Especificação formal (pt) Формальная спецификация (ru) Формальна специфікація (uk)
owl:sameAs freebase:Formal specification yago-res:Formal specification wikidata:Formal specification dbpedia-de:Formal specification dbpedia-es:Formal specification dbpedia-eu:Formal specification dbpedia-ja:Formal specification http://mg.dbpedia.org/resource/Famaritana_manarak'endrika dbpedia-pt:Formal specification dbpedia-ru:Formal specification dbpedia-simple:Formal specification dbpedia-uk:Formal specification https://global.dbpedia.org/id/SpJ2
prov:wasDerivedFrom wikipedia-en:Formal_specification?oldid=1097140681&ns=0
foaf:isPrimaryTopicOf wikipedia-en:Formal_specification
is dbo:knownFor of dbr:Joseph_Goguen
is dbo:wikiPageDisambiguates of dbr:Specification_(disambiguation) dbr:Formal
is dbo:wikiPageRedirects of dbr:Software_specification dbr:Formal_Specification dbr:Program_specification dbr:Specification_(computing)
is dbo:wikiPageWikiLink of dbr:Behavior_tree dbr:Program_synthesis dbr:List_of_computer_science_conferences dbr:Bertrand_Meyer dbr:Bracket dbr:Design_by_contract dbr:Algebraic_specification dbr:Algorithmic_program_debugging dbr:Jose_Meseguer dbr:Joseph_Goguen dbr:Per_Brinch_Hansen dbr:Perl dbr:Peter_Lucas_(computer_scientist) dbr:Reserved_word dbr:Don_Syme dbr:Inductive_programming dbr:Invariant-based_programming dbr:Lifecycle_Modeling_Language dbr:List_of_programming_language_researchers dbr:ScREC dbr:Praspel dbr:Protocol_engineering dbr:Coq dbr:Crowdsourcing_software_development dbr:Fuzzing dbr:Glossary_of_artificial_intelligence dbr:Glossary_of_computer_science dbr:Model_checking dbr:Mustache_(template_system) dbr:Precondition dbr:Communicating_sequential_processes dbr:Computer_science dbr:Z_User_Group dbr:Harlan_Mills dbr:Horn_clause dbr:Specification_(disambiguation) dbr:Specification_(technical_standard) dbr:Specification_language dbr:Theoretical_computer_science dbr:Microsoft_and_open_source dbr:Postcondition dbr:Action_semantics dbr:Whiley_(programming_language) dbr:Fuzzy_concept dbr:John_D._Gannon dbr:Lazy_systematic_unit_testing dbr:Software_factory dbr:Supercomputing_in_Pakistan dbr:Aaron_Swartz dbr:Abstract_state_machine dbr:Dafny dbr:E._Allen_Emerson dbr:Eric_Hehner dbr:First-order_logic dbr:Formal_verification dbr:PHP dbr:Formal_methods dbr:Formal_specification dbr:Prototype dbr:Reason dbr:Refinement_(computing) dbr:Reification_(computer_science) dbr:High-_and_low-level dbr:Is-a dbr:Requirements_engineering dbr:Software_specification dbr:ACM_Transactions_on_Programming_Languages_and_Systems dbr:Jim_Horning dbr:Jim_Woodcock dbr:Synchronous_programming_language dbr:TLA+ dbr:Jean-Raymond_Abrial dbr:Z_notation dbr:Model-based_specification dbr:Modeling_language dbr:Software_design dbr:Test_oracle dbr:Assertion_definition_language dbr:Automata-based_programming dbr:Automatic_bug_fixing dbr:B-Method dbr:Maplet dbr:Marie-Claude_Gaudel dbr:Business_rules_approach dbr:OneAPI_(compute_acceleration) dbr:X-Machine_Testing dbr:Software_requirements_specification dbr:Runtime_verification dbr:Unifying_Theories_of_Programming dbr:Vienna_Development_Method dbr:Extended_ML dbr:Formal dbr:Formal_Specification dbr:Formalization dbr:Programming_language dbr:Virtual_finite-state_machine dbr:X-machine dbr:Outline_of_software_engineering dbr:Object_language dbr:Rigorous_Approach_to_Industrial_Software_Engineering dbr:Program_specification dbr:Specification_(computing)
is dbp:knownFor of dbr:Joseph_Goguen
is foaf:primaryTopic of wikipedia-en:Formal_specification