Теормин-ФСВП, страница 2

To accomplish this, Dafny relies on high-level annotationsto reason about and prove correctness of code. The effect of a piece of code can be givenabstractly, using a natural, high-level expression of the desired behavior, which is easier andless error prone to write. Dafny then generates a proof that the code matches theannotations (assuming they are correct, of course!). Dafny lifts the burden of writing bugfree code into that of writing bug-free annotations. This is often easier than writing the code,because annotations are shorter and more direct. For example, the following fragment ofannotation in Dafny says that every element of the array is strictly positive:forall k: int :: 0 < k < a.Length ==> 0 < a[k]This says that for all integers k that are indices into the array, the value at that index isgreater than zero.

By writing these annotations, one is confident that the code is correct.Further, the very act of writing the annotations can help one understand what the code isdoing at a deeper level.In addition to proving a correspondence to user supplied annotations, Dafny proves thatthere are no run time errors, such as index out of bounds, null dereferences, division byzero, etc. This guarantee is a powerful one, and is a strong case in and of itself for the use ofDafny and tools like it. Dafny also proves the termination of code, except in speciallydesignated loops.ANSI/ISO C Specification LanguageThe ANSI/ISO C Specification Langage (ACSL) is a behavioral specification language for Cprograms.

The design of ACSL is inspired of JML. It also inherits a lot from the specificationlanguage of the source code analyzer Caduceus, a previous development of one of thepartners in the Frama-C project.ACSL can express a wide range of functional properties. The paramount notion in ACSL is thefunction contract.While many software engineering experts advocate the "function contract mindset" whendesigning complex software, they generally leave the actual expression of the contract torun-time assertions, or to comments in the source code. ACSL is expressly designed forwriting the kind of properties that make up a function contract.ACSL is a formal language. This means that the specifications written in ACSL can beautomatically manipulated by helper programs, in the same way that a programminglanguage is a formal language manipulated by a compiler, and by opposition to informallywritten comments that can only be useful to humans.ACSL allows to write contracts that range from the low-level (“this function expects a validpointer to int”) to the high-level (“this function expects a nonempty linked list of ints andreturns the greatest of these ints”).

It is expressive enough to write complete specificationsfor many functions, but it can also be used for writing partial specifications. Partialspecifications, of which the “expects a valid pointer to int” contract is a typical example, donot describe completely the expected behavior of the function.ACSL allows you to writecomplete specifications.But it does not force you to.Function contracts written as run-time assertions are almost always partial specifications,because a complete specification would be too annoying to write in the same language asthe programming language (indeed, most often this would mean programming the functiona second time).Jessie and Wp plug-ins use Hoare-style weakest precondition computations to formally proveACSL properties. The process can be quite automatic, thanks to external theorem proverssuch as Simplify, or Alt-Ergo, or more interactive, with the use of the Coq proof-assistant.Other plug-ins, such as the Value analysis plug-in may also contribute to the verification ofACSL properties.

They may also report static analysis results in terms of asserted new ACSLproperties inside the source code.ANSI/ISO C Specification Languagedeclarative with few imperative features. 2008The ANSI/ISO C Specification Language (ACSL) is a specification language for Cprograms, using Hoare style pre- and postconditions and invariants, that follows the designby contract paradigm. Specifications are written as C annotation comments to the Cprogram, which hence can be compiled with any C compiler.The current verification tool for ACSL is Frama-C.ACSL is a Behavioral Interface Specification Language (BISL).

It aims at specifying behavioralproperties of C source code./*@ requires \valid(p);@ assigns *p;@ ensures *p == \old(*p) + 1;@*/void incrstar (int *p);The contract is given by the comment which starts with /*@. Its meaning is as follows:the first line is a precondition: it states that function incrstar must be called with apointer p that points to a safely allocated memory location.Second line is a frame clause, stating that function incrstar does not modify anymemory location but the one pointed to by p.Finally, the ensures clause is a postcondition, which specifies that the value *p isincremented by one.Frama-CFormal verification, Static code analysisFrama-C stands for Framework for Modular Analysis of C programs.

Frama-C is a set ofinteroperable program analyzers for C programs. Frama-C enables the analysis of Cprograms without executing them.Frama-C relies on CIL (C Intermediate Language) to generate an abstract syntax tree.The abstract syntax tree supports annotations written in ANSI/ISO C SpecificationLanguage (ACSL).Frama-C can be used for the following purposes:to understand C code which you have not written.

In particular Frama-C enables to:observe a set of values, slice the program into shorter programs, navigate in theprogram.to prove formal properties on the code. Using specifications written in ANSI/ISO CSpecification Language enables to ensure properties of the code for any possiblebehavior. Frama-C handles floating point numbers [3].to enforce coding standards or code conventions on C source code, by means ofcustom plugin(s)[4].to instrument C code against some security flaws[5]PVS команды(split [fnum [depth]] )Conjunctively splits formula FNUM. If FNUM is -, + or *, then the first conjunctive sequentformula is chosen from the antecedent, succedent, or the entire sequent. Splittingeliminates any top-level conjunction, i.e., positive AND, IFF, or IF-THEN-ELSE, and negativeOR, IMPLIES, or IF-THEN-ELSE.flatten-- команда логики высказываний.

разбивает конъюнкцию вантецеденте на несколько отдельных антецендентов(предположенийдоказательства), каждый из которых соответствует одному из конъюнктов.Аналогично с дизъюнкцией в консеквенте.Disjunctively simplifies chosen formulas. It simplifies top-level antecedent conjunctions,equivalences, and negations, and succedent disjunctions, implications, and negations fromthe sequent.skolem-- создает новую переменную (точнее, подстановку переменной подквантором), заменяя ее в консеквенте, содержащем FORALL(квантор всеобщности),или антецеденте, содержащем EXISTS(квантор существования).(skolem fnum constant [skolem-typepreds? dont-simplify?])Replaces the universally quantified variables in FNUM with new skolem constants inCONSTANTS.

If SKOLEM-TYPEPREDS? is T, then typepreds will be generated for theintroduced constants. If DONT-SIMPLIFY? is T, then the simplifications that occurautomatically during substitution are suppressed.Example: (skolem 1 ("A" "B"))See also SKOLEM!, SKOSIMP, SKOSIMP*.skolem! сам выбирает имя, skosimp = skolem + flatten, skosimp* = skosimp в циклеinst-- Подстановка в формулу. Существует автоматизированный вариант(inst?), подставляющий в самую первую возможную формулу что взбредет. Работаеттолько в самых простейших случаях.Подстановки возможны либо в FORALL в предположении (антеценденте), либо вEXISTS в цели доказательства(консеквенте).(inst fnum terms*)Instantiates the top quantifier in formula FNUMassert-- автопрувер №1.

Вроде как относится к логике вычислений. На сайтеКорна это значится как equational logic, хотя в остальный местах как equality logic.умеет упрощать, складывать, вычитать, умножать, делить и доказывать очевидныевещи.(assert/$ &optional (fnums *) rewrite-flag flush? linear?cases-rewrite? (type-constraints? t) ignore-prover-output?(let-reduce? t) quant-simp? implicit-typepreds?) :Simplifies/rewrites/records formulas in FNUMS using decision procedures. Variant ofSIMPLIFY with RECORD? and REWRITE? flags set to T. If REWRITE-FLAG is RL(LR) then onlylhs(rhs) of equality is simplified. If FLUSH? is T then the current asserted facts are deleted forefficiency. LINEAR? is currently ignored.

If CASES-REWRITE? is T, then the selections andelse parts of a CASES expression are simplified,otherwise, they are only simplified when simplification selects a case. See also SIMPLIFY,RECORD, DO-REWRITE.Examples:(assert): Simplifies, rewrites, and records all formulas.(assert -1 :rewrite-flag RL): Apply assert to formula -1 leavingRHS untouched if the formula is an equality.(assert :flush? T): Apply assert after flushing existing decision proceduredatabase.prop-- автопрувер №2, автоматическая стратегия для логики высказываний.Преобразования по типу правил де Моргана, если я все правильно понимаюA black-box rule for propositional simplification.grind-- автопрувер №3.Если не сможет доказать, то может превратить верноеутверждение в недоказуемое.lemma, use -- включение в список предположений(антецедентов) леммы/аксиомы поимени.

По моему опыту, use ~ (lemma “name”)(inst?)replace-- подстановка предположений(они же assumption, они же антецеденты).Может подставлять переменные, вычисленные в одном из предположений, в другое.Также умеет работать с неравенствами.case-- Разбивает доказательство на 2 случая -- если выполняется некотороебулевское выражение или выполняется его отрицание. Утверждений может бытьнесколько.Splits according to the truth or falsity of the formulas. (CASE a b c) on a sequent A |- Bgenerates subgoals:a, b, c, A |- B;a, b, A |- c, B;a, A |- b, B;A |- a, B.See also CASE-REPLACE, CASE*lift-if(lift-if [fnums [updates? t] ])Lifts IF occurrences to the top of chosen formulas. CASES, COND, and WITH applications, aretreated as IF occurrences.