11 research outputs found
Event-B code generation: type extension with theories
No full textThe Event-B method is a formal modelling approach; our interest is the final step, of generating code for concurrent programs, from Event-B. Our Tasking Event-B tool integrates Event-B to facilitate code generation. The theory plug-in allows mathematical extensions to be added to an Event-B development. When working at the implementation level we need to consider how to translate the newly added types and operators into code. In this paper, we augment the theory plug-in, by adding a Translation Rules section to the tool. This enables us to define translation rules that map Event-B formulas to code. We illustrate the approach using a small case study, where we add a theory of arrays, and specify translation rules for generating Ada code
Towards a practically extensible Event-B methodology
No full textFormal modelling is increasingly recognised as an important step in the development of reliable computer software. Mathematics provide a solid theoretical foundation upon which it is possible to specify and implement complex software systems. Event-B is a formalism that uses typed set theory to model and reason about complex systems. Event-B and its associated toolset, Rodin, provide a methodology that can be incorporated into the development process of software and hardware. Refinement and mathematical proof are key features of Event-B that can be exploited to rigorously specify and reason about a variety of systems. Successful and usable formal methodologies must possess certain attributes in order to appeal to end-users. Expressiveness and extensibility, among other qualities, are of major importance. In this thesis, we present techniques that enhance the extensibility of: (1) the mathematical language of Event-B in order to enhance expressiveness of the formalism, and (2) the proving infrastructure of the Rodin platform in order to cope with an extensible mathematical language. This thesis makes important contributions towards a more extensible Event-B methodology.Firstly, we show how the mathematical language of Event-B can be made extensible in a way that does not hinder the consistency of the underlying formalism. Secondly, we describe an approach whereby the prover used for reasoning can be augmented with proof rules without compromising the soundness of the framework. The theory component is the placeholder for mathematical and proof extensions. The theoretical contribution of this thesis is the study of rewriting in the presence of partiality. Finally, from a practical viewpoint, proof obligations are used to ensure soundness of user-contributed extensions
Practical Theory Extension in Event-B
No full textAbstract. The Rodin tool for Event-B supports formal modelling and proof using a mathematical language that is based on predicate logic and set theory. Although Rodin has in-built support for a rich set of operators and proof rules, for some application areas there may be a need to extend the set of operators and proof rules supported by the tool. This paper outlines a new feature of the Rodin tool, the theory component, that allows users to extend the mathematical language supported by the tool. Using theories, Rodin users may define new data types and polymorphic operators in a systematic and practical way. Theories also allow users to extend the proof capabilities of Rodin by defining new proof rules that get incorporated into the proof mechanisms. Soundness of new definitions and rules is provided through validity proof obligations.
On an extensible rule-based prover for event-B
No full textEvent-B is a formalism for discrete system modelling. The Rodin platform provides a toolset to carry out specification, refinement and proof in Event-B. The importance of proofs as part of formal modelling cannot be emphasised enough, and as such, it is imperative to provide effective tool support for it. An important aspect of this support is the extensibility of the prover, and more pressingly, how its soundness is preserved while allowing extensibility. Rodin has a limited support for adding rules as this requires (a) a deep understanding of the internal architecture and (b) knowledge of the Java language. Our approach attempts to provide support for user-defined proof rules. We initially focus on supporting rewrite rules to enhance the rewriting capabilities of Rodin. To achieve this objective, we introduce a theory construct distinct from contexts and machines. The theory construct provides a platform for the users to define rewrite rules both conditional and unconditional. As part of rule definition, users decide whether the rule is to be applied automatically or interactively. Each defined rule gives rise to proof obligations that serve to verify its conservativity. In this respect, it is required that validity and well-definedness are preserved by rules. After the conservativity of all rules contained in a theory is established, the theory can then be deployed and available to the proving activity. In order to apply rewrite rules, it is necessary to single out applicable rules to any given sequent. This is achieved through a pattern matching mechanism which is implemented as an extension to Rodin. Our approach has two advantages. Firstly, it offers a uniform mechanism to add proof rule without the need to write Java code. Secondly, it provides a means to verify added rules using proof obligations. Our work is still in progress, and research has to be carried out to (a) cover a larger set of rewrite and inference rules, and (b) provide guidelines to help the theory developer with deciding whether a given rule should be applied automatically
Ensuring extensibility within code generation
No full textMaking the step from Event-B to code is a process that can be aided through automatic code generation. The code generation plug-in for Rodin is a new tool for translating Event-B models to concurrent programmes. However users of such a tool will likely require a diverse range of target languages and target platforms, for which we do not currently provide translations. Some of these languages may be subtly different to existing languages and only have modest differences between the translation rules, for example C and C++, whilst others may have more fundamental differences. As the translation from Event-B to executable code is non-trivial and to reduce the likelihood of error, we want to generalise as much of the translation as possible so that existing translation rules are re-used. Therefore significant effort is needed to ensure that such a translation tool is extensible to allow additional languages to be included with relative ease. Here we concentrate on translation from a previously defined intermediary language, called IL1, which Event-B translates to directly
Rewriting and Well-Definedness within a Proof System
No full textTerm rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B
Rewriting and Well-Definedness within a Proof System
No full textTerm rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.</jats:p
The Role of the School Counselor in Diagnosing the Aggressive Behavior and Learning Disabilities: A Case Study in Algeria
No full textObservation is among the primary methods and tools used for data collection. It allows the researchers to do so when the data are generated in the real world and participate in the process as participant observers. In this line, the researcher records what he notices. Therefore, the observation is mainly related to the qualitative research and data. Nevertheless, the quantitative indices are a form of observation at the superficial level. It is also better to link the observation with the quantitative research design. This study aims to contribute to the understanding of observation in scientific research due to the low use of this technique in educational and psychological scientific research. Thus, the researcher carried out a theoretical reading of this tool and used the clinical method by presenting a practical model of observation to diagnose the psychological and educational issues in the school milieu. In this context, we studied a case that showed aggressive behaviors and relied on other tools to help diagnose the problem, such as the Harris Good-Enough test of man drawing and the scale of measuring learning disabilities made by Maamria Bashir in 2005. Findings show the efficiency of the observation in diagnosing the problem of aggressive behavior in the school milieu. Based on the results, we provided a set of recommendations and suggestions
