The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
In order to improve software quality, specifiers can take advantage of the use of formal methods in the software development process. With regard to requirements specifications, attempts in this sense have been successfully made. We claim that also in the design phase a formal approach could lead to several benefits, such as the possibility of formally checking if the produced documents satisfy initial...
Most computers are used in an organisational setting and most organisational information systems are database systems. A database system is one in which the simple statements far outnumber the complex ones, to the extent that a special database management system is required to enable sufficiently rapid access to the data thus stored. SQL is the standard language for database access and manipulation...
This paper describes a project which is using Z in the field of artificial intelligence (AI) to provide a defining framework for agency and autonomy. Specifically, the use of Z has provided a means for escaping from the terminological chaos surrounding agency and autonomy that is prevalent not just in the AI community, but also in other areas of computer science. We outline how we have developed a...
This paper presents an experience on the use of objectoriented formal specifications in the process of software development for artificial neural networks. A formal specification of artificial neural networks using the MooZ language is presented. This specification of class hierarchies shows the gradual inclusion of neural network concepts such that new models or paradigms are easily incorporated...
A report is given on work undertaken to produce a structured specification in Z of a model which aims to capture the essential abstractions of hypertext systems. The specification is presented in part and the potential value of this specification to the hypertext community is explored and discussed. We argue that this specification provides a framework for hypertext systems in that it provides: explicit...
Mechanization makes it feasible to calculate properties of formally specified systems. This ability creates new opportunities for using formal methods as an exploratory tool in system design. Achieving enough efficiency to make this practical raises challenging problems in automated deduction. These challenges can be met only by approaches that integrate consideration of its mechanization into the...
We present a simple example to illustrate the algebraic, constructive style of specification and proof used in the Irish School of the VDM(VDM♣). The example exploits a new and fundamental result which we have used frequently in VDM♣. Our illustration also demonstrates a novel approach within in the VDM tradition which harnesses...
The PROST-Objects project has developed a method for formally specifying tests. The method is based on systematic abstraction from a ‘state-plusoperation’ style specification. It is explained here, and illustrated with a small example. Test developers can use this method, along with their own skills for choosing good tests, to produce a suite of formal test specifications. The project has also developed...
Formal Specifications become more and more important in the development of software, especially, but not only in the area of high integrity systems. Testing as a method to validate the functionality of a system against the specification will keep its justification also in a development process using formal specifications. We demonstrate, where the problems lie when carrying out software integration...
If Z specifications are used as requirements specifications then test result evaluation leads to evaluation of schema predicates in states that are reached by the test. For automation of this approach Z operational schemas must be translated into programs that perform schema predicate evaluation. Predicate evaluation is straightforward; expressions are replaced by their values, logical connectives...
Schemas are a part of the Z notation, but not well integrated into its mathematical language. The paper shows how to make Z more unified and more flexible by removing the distinction between expression and schemaexpression. The Cartesian product can also be taken as a special case of a schema. As examples, it is shown how to embed operation schemas into the mathematical language, and how schema...
This paper investigates the issue of structuring Z specifications. It uses examples from a large specification to examine both conventions for using Z and notational extensions including Object-Z. Because of the importance of good structure within a specification, specifiers need to be aware of a range of techniques and where each is applicable.
Standards, if widely accepted, encourage the development of tools and techniques to process objects conforming to that standard. This paper describes a number of experiments using available tools to process text containing Z specifications adhering to the existing Z Interchange Format. The experiments resulted in tools that could be used in specific programming environments where Z was used to describe...
Specifications are useful because they allow reasoning about objects without concern for their implementations. Type hierarchies are useful because they allow types that share common properties to be designed as a family. This paper is concerned with the interaction between specifications and type hierarchies. We present a way of specifying types, and show how some extra information, in addition to...
We tackle an under-explored question in Z semantics; what does an operation schema mean? We explain why this is important by describing our requirement to specify objects with active and passive behaviours. We show that one of the interpretations we uncover in order to represent active behaviour can also considerably simplify object-oriented inheritance.
This paper presents a logic for Object-Z which extends W, the logic for Z adopted as the basis of the deductive system in the Z Base Standard. The logic provides a basis on which tool support for reasoning about Object-Z specifications can be developed. It also formalises the intended meaning of Object-Z constructs and hence provides an abstract, axiomatic semantics of the language.
The purpose of this paper is to give a formal semantics for a language which includes type extension. Used in association with pointer variables, this forms the basis of object-orientation in the languages Oberon and Oberon-2 which have evolved from Modula-2. The focus is on the meaning of assignment because this is the important difference between such languages and the strongly-typed Pascal family...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.