-
Notifications
You must be signed in to change notification settings - Fork 42
Glossary
Octavian Mircea Sebe edited this page Mar 11, 2021
·
1 revision
- (noun, acronym) Bounded model checking. Execute the program on all paths for a given number of steps (a.k.a. bound), attempting to identify given properties (bugs, unexpected behaviours, and so on) in the execution graph.
- (adjective)
A pattern is constructor-like if logical equality is syntactic equality. A
pattern is constructor-like if it is logically equal (in the
\equals
sense) to another constructor-like pattern if and only if the patterns are syntactically equal. The constructor-like patterns of a sort comprise a normal form of elements in that sort. - (adjective) A symbol is constructor-like if it may form the head of a constructor-like application pattern (in the sense defined above). Roughly, this means the symbol has injectivity and no-confusion axioms.
- (noun) An application symbol that, when applied to function-like patterns, produces function-like patterns.
- (noun/adjective) A function-like pattern.
- (adjective)
A function-like pattern can have at most one value, i.e. it satisfies
(∃x . x=φ) ∨ ¬⌈φ⌉
.
- (adjective)
A functional pattern has exactly one value, i.e. it satisfies
(∃x . x=φ)
.
- (noun) A syntactic element constructed according to the rules described in the semantics-of-k document.
- (noun) The internal representation of such a syntactic element. It may have constructs which cannot be represented directly into syntactic elements (e.g. map domain values), but it is expected that it is possible to create an equivalent syntactic representation.
- (noun) A pattern that can be evaluate only to top and bottom. Application patterns that can only evaluate to top and bottom are hard to identify, so some of the code that identifies predicates fails on these. Whenever a substitution can be extracted efficiently, the "predicate" term may refer to the non-substitution part of the predicate.
- (noun, acronym) Semantics-based compilation. Compilation that uses the semantics of the language to analyze the behaviour of the program (e.g. through symbolic execution), and uses what it learned to improve the compilation result.
- (noun)
A symbol with the
sortInjection
attribute. The sort injection symbol is used to represent the K sub-sort relation in Kore: K sorts contain symbols and sorts (their sub-sorts), but Kore sorts contain only symbols; the sort injection symbol wraps patterns of a sub-sort so they can be included (injected) into the super-sort. Two important properties follow from this definition: first, that sort injection symbols are injective; second, that the sort injection symbol from a particular sub-sort is distinct (in the no-confusion-different-constructors sense) from the super-sort's constructors. - (noun)
A sort injection is a pattern of the form,
where
inj{Sub{}, Super{}}(φ:Sub{})
inj{Sub{}, Super{}}
is a sort injection symbol (described above). Where the K sortSuper
containsSub
, the patternφ
with least-sortSub
can appear anywhere that a term of sortSuper
is required. In Kore, this is represented with the injection above because all sorts are regarded as distinct.
- (noun)
A predicate of the form
x1=φ1 ∧ x2=φ2 ∧ ... ∧ xn=φn
wherexi
are variables andφi
are patterns.
- (noun) A pattern of a specific type. A term pattern is usually constructed with variables and function application patterns, but, in many cases, it is used for any pattern with the expectation that it will be reduced, as much as reasonably possible, to a variable-application from.