the behaviour of systems is determined by their implementation in some form of source code. While behaviour itself is complex and its detailed semantics are hard to describe by means of lower level than a programming ...
详细信息
ISBN:
(纸本)0769517692
the behaviour of systems is determined by their implementation in some form of source code. While behaviour itself is complex and its detailed semantics are hard to describe by means of lower level than a programming or specification language, the structure of dynamic input/output behaviour is limited by the system logic and fixed during operation in most cases. Certain aspects of system behavior can be captured by regular expressions that define the possible input/output behaviors of the system. A more refilled kind of regular expression can be constructed that does not only represent I/O interleaving but also the location and type of every particular I/O event. this article describes the generation of such expressions and shows how they, can be used to aid classic verification by, testing, as well as in a criterion to assess the quality of given test case sets. Additionally, a method is sketched to falsify the behavioural identity of systems using the presented approach. Finally, a tool to apply the presented ideas in verification practice on MC68HC705J1A microcontroller programs is overviewed.
Meta-programming languages provide infrastructure to generate and execute object programs at run-time. In a typed setting, they contain a modal type constructor which classifies object code. these code types generally...
详细信息
ISBN:
(纸本)9781581134872
Meta-programming languages provide infrastructure to generate and execute object programs at run-time. In a typed setting, they contain a modal type constructor which classifies object code. these code types generally come in two flavors: closed and open. Closed code expressions can be invoked at run-time, but the computations over them are more rigid, and typically produce less efficient residual object programs. Open code provides better inlining and partial evaluation of object programs, but once constructed, expressions of this type cannot in general be evaluated. Recent work in this area has focused on combining the two notions into a sound system. We present a novel way to achieve this. It is based on adding the notion of names from the work on Nominal logic and FreshML to the lambda(square)-calculus of proof terms for the necessity fragment of modal logic S4. the resulting language provides a more fine-grained control over free variables of object programs when compared to the existing languages for meta-programming. In addition, this approach lends itself well to addition of intensional code analysis, i.e. ability of meta programs to inspect and destruct object programs at run-time in a type-safe manner, which we also undertake.
Negation as failure is an important language feature within the logicprogramming paradigm. the natural notion generalizing negation as failure in a functionallogic setting is that of finite failure of reduction. In ...
详细信息
In typed logicprogramming, the head condition states that for each clause defining a predicate p, the arguments of the clause head must have the declared type of p, rather than a proper polymorphic instance. In typed...
详细信息
this paper suggests functionalprogramming languages with coinductive types as suitable devices for prototyping process calculi. the proposed approach is independent of any particular process calculus and makes explic...
详细信息
We introduce a handful of software design patterns for functionallogic languages. Following usual approaches, for each pattern we propose a name and we describe its intent, applicability, structure, consequences, etc...
详细信息
Many frameworks of logicprogramming have been proposed to manage uncertain information in deductive databases and expert systems. Roughly, on the basis of how uncertainty is associated to facts and the rules in a pro...
详细信息
this paper explores a seeminglyv ery simple idea—an operation for extending a term with extra (start or end) arguments to yield a new term. this allows the definition a varietyof structural operators that provide the...
详细信息
Experience using constraint programming to solve real-life problems has shown that finding an efficient solution to the problem often requires experimentation with different constraint solvers or even building a probl...
详细信息
the behaviour of systems is determined by their implementation in some form of source code. While behaviour itself is complex and its detailed semantics are hard to describe by means of lower level than a programming ...
详细信息
the behaviour of systems is determined by their implementation in some form of source code. While behaviour itself is complex and its detailed semantics are hard to describe by means of lower level than a programming or specification language, the structure of dynamic input/output behaviour is limited by the system logic and fixed during operation in most cases. Certain aspects of system behavior can be captured by regular expressions that define the possible input/output behaviors of the system. A more refined kind of regular expression can be constructed that does not only represent I/O interleaving but also the location and type of every particular I/O event. this article describes the generation of such expressions and shows how they can be used to aid classic verification by testing, as well as in a criterion to assess the quality of given test case sets. Additionally, a method is sketched to falsify the behavioural identity of systems using the presented approach. Finally, a tool to apply the presented ideas in verification practice on MC68HC705J1A microcontroller programs is overviewed.
暂无评论