This HTML5 document contains 51 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n6https://global.dbpedia.org/id/
yagohttp://dbpedia.org/class/yago/
dbpedia-ruhttp://ru.dbpedia.org/resource/
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
wikipedia-enhttp://en.wikipedia.org/wiki/
provhttp://www.w3.org/ns/prov#
dbchttp://dbpedia.org/resource/Category:
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
goldhttp://purl.org/linguistics/gold/
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbr:Invariant-based_programming
rdf:type
yago:Cognition100023271 yago:WikicatProgrammingParadigms yago:Paradigm113804375 yago:Relation100031921 yago:GrammaticalRelation113796779 yago:Method105660268 yago:Ability105616246 yago:LinguisticRelation113797142 yago:Abstraction100002137 yago:Inflection113803782 dbo:Software yago:PsychologicalFeature100023100 yago:Know-how105616786 yago:WikicatFormalMethods
rdfs:label
Invariant-based programming Инвариантное программирование
rdfs:comment
Invariant-based programming is a programming methodology where specifications and invariants are written before the actual program statements. Writing down the invariants during the programming process has a number of advantages: it requires the programmer to make their intentions about the program behavior explicit before actually implementing it, and invariants can be evaluated dynamically during execution to catch common programming errors. Furthermore, if strong enough, invariants can be used to prove the correctness of the program based on the formal semantics of program statements. A combined programming and specification language, connected to a powerful formal proof system, will generally be required for full verification of non-trivial programs. In this case a high degree of autom Инвариантное программирование — методология программирования, при которой спецификации и инварианты описываются до исполняемых операторов программы. Описание инвариантов во время процесса программирования имеет ряд преимуществ: требует от программиста сформировать идеи о поведении программы явно до того, как их реализовать, и инварианты могут быть вычислены в процессе выполнения, что помогает выявить общие ошибки программирования. Более того, достаточно сильные инварианты могут быть использованы для формальной проверки программы на корректность, основываясь на формальной семантике тела программы. Однако для полной проверки нетривиальных программ потребуется язык программирования, совмещённый со спецификациями и объединённый в мощную систему формальных доказательств. В этом случае высокая с
dcterms:subject
dbc:Formal_methods dbc:Programming_paradigms
dbo:wikiPageID
4160992
dbo:wikiPageRevisionID
975976911
dbo:wikiPageWikiLink
dbr:Formal_specification dbr:Eiffel_(programming_language) dbc:Formal_methods dbr:For_loop dbr:Edsger_Dijkstra dbr:Invariant_(computer_science) dbr:While_loop dbr:Formal_semantics_of_programming_languages dbr:Formal_verification dbr:If_statement dbr:Ralph-Johan_Back dbc:Programming_paradigms dbr:John_C._Reynolds
owl:sameAs
n6:4nk4o freebase:m.0bmdnr yago-res:Invariant-based_programming dbpedia-ru:Инвариантное_программирование wikidata:Q6059500
dbo:abstract
Инвариантное программирование — методология программирования, при которой спецификации и инварианты описываются до исполняемых операторов программы. Описание инвариантов во время процесса программирования имеет ряд преимуществ: требует от программиста сформировать идеи о поведении программы явно до того, как их реализовать, и инварианты могут быть вычислены в процессе выполнения, что помогает выявить общие ошибки программирования. Более того, достаточно сильные инварианты могут быть использованы для формальной проверки программы на корректность, основываясь на формальной семантике тела программы. Однако для полной проверки нетривиальных программ потребуется язык программирования, совмещённый со спецификациями и объединённый в мощную систему формальных доказательств. В этом случае высокая степень автоматизации доказательств также возможна. В императивных языках программирования основные организующие структуры — это блоки управления потоком выполнения, такие как цикл со счётчиком (for), цикл с предусловием (while) и условные операторы (if). Такие языки плохо подходят для инвариантного программирования, поскольку они принуждают программиста принимать решения об управлении потоком до написания инвариантов. Более того, такие языки программирования не имеют нужной поддержки для описания спецификаций и инвариантов, поскольку в них нет кванторов и они не могут выражать свойства высшего порядка. Идея разработки программы совместно с её доказательством восходит к идеям Э. Дейкстры. Написание инвариантов перед блоком операторов описывалось в том числе такими исследователями как M. H. van Emden, и . Invariant-based programming is a programming methodology where specifications and invariants are written before the actual program statements. Writing down the invariants during the programming process has a number of advantages: it requires the programmer to make their intentions about the program behavior explicit before actually implementing it, and invariants can be evaluated dynamically during execution to catch common programming errors. Furthermore, if strong enough, invariants can be used to prove the correctness of the program based on the formal semantics of program statements. A combined programming and specification language, connected to a powerful formal proof system, will generally be required for full verification of non-trivial programs. In this case a high degree of automation of proofs is also possible. In most existing programming languages the main organizing structures are control flow blocks such as for loops, while loops and if statements. Such languages may not be ideal for invariants-first programming, since they force the programmer to make decisions about control flow before writing the invariants. Furthermore, most programming languages do not have good support for writing specifications and invariants, since they lack quantifier operators and one can typically not express higher order properties. The idea of developing the program together with its proof originated from E.W. Dijkstra. Actually writing invariants before program statements has been considered in a number of different forms by M.H. van Emden, J.C. Reynolds and R-J Back.
gold:hypernym
dbr:Methodology
prov:wasDerivedFrom
wikipedia-en:Invariant-based_programming?oldid=975976911&ns=0
dbo:wikiPageLength
2258
foaf:isPrimaryTopicOf
wikipedia-en:Invariant-based_programming
Subject Item
dbr:Invariant_Based_Programming
dbo:wikiPageWikiLink
dbr:Invariant-based_programming
dbo:wikiPageRedirects
dbr:Invariant-based_programming
Subject Item
dbr:Invariant_based_programming
dbo:wikiPageWikiLink
dbr:Invariant-based_programming
dbo:wikiPageRedirects
dbr:Invariant-based_programming
Subject Item
wikipedia-en:Invariant-based_programming
foaf:primaryTopic
dbr:Invariant-based_programming