This paper is a description of a simple operating system, which runs in a virtual machine (implemented on a real machine by an interpreter). OS6 copes with only one user at a time, and is not a multi-programming syste...
The Z notation has been developed at the programmingresearch Group at the Oxford University Computing laboratory and elsewhere for over a decade. It is now used by industry as part of the software (and hardware) deve...
详细信息
ISBN:
(数字)9781447135562
ISBN:
(纸本)9783540198185
The Z notation has been developed at the programmingresearch Group at the Oxford University Computing laboratory and elsewhere for over a decade. It is now used by industry as part of the software (and hardware) development process in both Europe and the USA. It is currently undergoing BSI standardisation in the UK, and has been proposed for ISO standardisation internationally. In recent years researchers have begun to focus increasingly on the development of techniques and tools to encourage the wider application of Z and other formal methods and notations. This volume contains papers from the Seventh Annual Z User Meeting, held in London in December 1992. In contrast to previous years the meeting concentrated specifically on industrial applications of Z, and a high proportion of the participants came from an industrial background. The theme is well represented by the four invited papers. Three of these discuss ways in which formal methods are being introduced, and the fourth presents an international survey of industrial applications. It also provides a reminder of the improvements which are needed to make these methods an accepted part of software development. In addition the volume contains several submitted papers on the industrial use of Z, two of which discuss the key area of safety-critical applications. There are also a number of papers related to the recently-completed ZIP project. The papers cover all the main areas of the project including methods, tools, and the development of a Z Standard, the first publicly-available version of which was made available at the meeting. Finally the volume contains a select Z bibliography, and section on how to access information on Z through ***.z, the international, computer-based USENET newsgroup.;provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students andalso potential industrial users of Z.
This volume contains papers from the Eighth Z User Meeting, to be held at the University of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particul...
详细信息
ISBN:
(数字)9781447134527
ISBN:
(纸本)9783540198840
This volume contains papers from the Eighth Z User Meeting, to be held at the University of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particular reference to practical application. These issues include education, standards, tool support, and interaction with other design paradigms such as consideration of real-time and object-oriented approaches to development. Among the actual topics covered are: the formal specification in Z of Defence Standard 00-56; formal specification of telephone features; specifying and interpreting class hierarchies in Z; and software quality assurance using the SAZ method.;provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students and also potential industrial users of Z.
作者：
Birnbaum, L.S.Bukzin, E.A.Saroyan, J.R.Leon S. Birnbaum holds a B.S. degree in Chemistry from City College of New York. He has completed graduate work in Chemistry at the University of Maryland and Temple University
and in Technology and Management at American University. He has been with the Navy Department Washington since 1949 and is currently Head of the Coatings and Chemistry Branch of the Materials Development and Application Office of the Naval Ship Engineering Center. Responsibilities of this Branch include such items as coatings corrosion control techniques insulation chemical cleaning water treatment toxicology and detection and decontamination of biological and chemical warfare agents. Prior to this Mr. Birnbaum was employed in the Industrial Test Laboratory Philadelphia Naval Shipyard from 1938 to 1949. Work during this period included supervision of a section which inspected paints and allied materials and petroleum products to determine their suitability for Naval use and direction of research in fire retardant treatments. He is a member of the American Chemical Society
Washington Paint Technical Group. National Association of Corrosion Engineers and the American Society of Naval Engineers. Mr. Bukzin is a research and development program manager in the Naval Ship Systems Command of the Department of the Navy in the fields of non-metallic materials
fuels lubricants cold weather operations and several other areas. He is a graduate chemical engineer from New York University with additional training in naval architecture and management which culminated in his participation in the Senior Development Program at Cornell University during the summer of 1960. He has been employed by the Command and its predecessor for the past 2b years and has been in his present position of R&D planning and programming for the past six years. Prior to that his major technical responsibilities were in the field of elastomers and their applications. He received several awards and published a number of papers during those years. Mr. Bukzin is a me
Report on paints used on surface ships and submarines for protection against corrosion and prevention of fouling, and on work connected with development and evaluation of such coatings;experiences with "hot plast...
详细信息
Report on paints used on surface ships and submarines for protection against corrosion and prevention of fouling, and on work connected with development and evaluation of such coatings;experiences with "hot plastic", "cold plastic" and vinyl paints;hazards in use of vinyl paints and safety precautions;test techniques;new toxics (which are only kind so far satisfactory antifouling formulations) under test.
作者：
Robson, J.M.Oxford University
Programming Research Group Oxford University Computing Laboratory Oxford United Kingdom
Dynamic storage allocation using fixed blocks is usually inefficient in its use of store. The amount of store needed depends on the allocation strategy used. It is proved that for any strategy the amount of store need...
详细信息
In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value ...
详细信息
ISBN:
(数字)9781447132035
ISBN:
(纸本)9783540197805
In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value of x which satisfies it. Similarly it is possible to specify objects using the formal specification language Z [3,4], which can not possibly exist. Such specifications are called inconsistent and can arise in a number of ways. Example 1 The following Z specification of a functionf, from integers to integers "f x : ~ 1 x ~ O· fx = x + 1 (i) "f x : ~ 1 x ~ O· fx = x + 2 (ii) is inconsistent, because axiom (i) gives f 0 = 1, while axiom (ii) gives f 0 = 2. This contradicts the fact that f was declared as a function, that is, f must have a unique result when applied to an argument. Hence no suchfexists. Furthermore, iff 0 = 1 andfO = 2 then 1 = 2 can be deduced! From 1 = 2 anything can be deduced, thus showing the danger of an inconsistent specification. Note that all examples and proofs start with the word Example or Proof and end with the symbol.1.
A " basic English" to enable editors, writers, librarians, educators, and others to instruct computers to perform mechanical text processing conveniently has been defined (see Tables II to V for partial summ...
详细信息
A " basic English" to enable editors, writers, librarians, educators, and others to instruct computers to perform mechanical text processing conveniently has been defined (see Tables II to V for partial summary). It has been given the name SNAP (Stylized Natural Procedural) language for reference. A processor that executes procedures expressed in a subset of this language has worked for some months on several computers. It was used successfully last semester by 40 students with humanities background, in a graduate course in the School of Library Service of Columbia University, for elementary mechanized library and documentation tasks. The processor for the larger subset of the language shown in Tables II to V now works, and is being applied to several practical problems. The processor for the full language is being completed. A SNAP procedure consists of a succession of well-formed English sentences of a few simple types. Most of these begin with imperative verbs that are concerned with input and output operations, and with the manipulation of strings of characters, numbers, and arrays of strings and numbers. Conditional sentences begin with IF. Several constructions that extract and concatenate portions of strings and lists of strings are used in the objects of SNAP sentences. The SNAP processor is written (apart from specialized input-output routines) in FORTRAN IV. It deals directly with some 25 "built-in" verbs, and will allow the user to define further verbs by subroutines that are also written in SNAP.
暂无评论