The B method is one of the few formal methods with commerciallly available tool support. It has been succesfully applied in the development of several industrial applications. In this paper we present an application of the B-Method to a new domain, namely language development. We have developed an approach for translating a language with a structural operational semantics into B specifications. The language semantics is specified in separate B machines, that act as an interpreter for programs in the language. The programs, represented as abstract syntax trees, can then automatically be translated into B specifications. We have used the approach in the context of Rialto, a language for multiple models of computation. We show how Rialto programs are translated into B machines, and how the different scheduling policies that are used to interpret concurrency can be also be represented as B machines. We also discuss some shortcomings of the approach and the B-Tools that we have available.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.