Object-Z

Last updated

Object-Z [1] is an object-oriented extension to the Z notation developed at the University of Queensland, Australia.

Contents

Object-Z extends Z by the addition of language constructs resembling the object-oriented paradigm, most notably, classes. Other object-oriented notions such as polymorphism and inheritance are also supported.

While not as popular as its base language Z, Object-Z has still received significant attention in the formal methods community, and research on aspects of the language are ongoing, including hybrid languages using Object-Z, [2] [3] tool support (e.g., through the Community Z Tools project) and refinement calculi. [4]

See also

Related Research Articles

Spaghetti code is a pejorative phrase for unstructured and difficult-to-maintain source code. Spaghetti code can be caused by several factors, such as volatile project requirements, lack of programming style rules, and software engineers with insufficient ability or experience.

In information science, an ontology encompasses a representation, formal naming, and definition of the categories, properties, and relations between the concepts, data, and entities that substantiate one, many, or all domains of discourse. More simply, an ontology is a way of showing the properties of a subject area and how they are related, by defining a set of concepts and categories that represent the subject.

In software engineering, a software design pattern is a general, reusable solution to a commonly occurring problem within a given context in software design. It is not a finished design that can be transformed directly into source or machine code. Rather, it is a description or template for how to solve a problem that can be used in many different situations. Design patterns are formalized best practices that the programmer can use to solve common problems when designing an application or system.

In software engineering and development, a software metric is a standard of measure of a degree to which a software system or process possesses some property. Even if a metric is not a measurement, often the two terms are used as synonyms. Since quantitative measurements are essential in all sciences, there is a continuous effort by computer science practitioners and theoreticians to bring similar approaches to software development. The goal is obtaining objective, reproducible and quantifiable measurements, which may have numerous valuable applications in schedule and budget planning, cost estimation, quality assurance, testing, software debugging, software performance optimization, and optimal personnel task assignments.

<span class="mw-page-title-main">Multi-agent system</span> Built of multiple interacting agents

A multi-agent system is a computerized system composed of multiple interacting intelligent agents. Multi-agent systems can solve problems that are difficult or impossible for an individual agent or a monolithic system to solve. Intelligence may include methodic, functional, procedural approaches, algorithmic search or reinforcement learning.

<span class="mw-page-title-main">Meta-process modeling</span>

Meta-process modeling is a type of metamodeling used in software engineering and systems engineering for the analysis and construction of models applicable and useful to some predefined problems.

Architecture description languages (ADLs) are used in several disciplines: system engineering, software engineering, and enterprise modelling and engineering.

Software visualization or software visualisation refers to the visualization of information of and related to software systems—either the architecture of its source code or metrics of their runtime behavior—and their development process by means of static, interactive or animated 2-D or 3-D visual representations of their structure, execution, behavior, and evolution.

End-user development (EUD) or end-user programming (EUP) refers to activities and tools that allow end-users – people who are not professional software developers – to program computers. People who are not professional developers can use EUD tools to create or modify software artifacts and complex data objects without significant knowledge of a programming language. In 2005 it was estimated that by 2012 there would be more than 55 million end-user developers in the United States, compared with fewer than 3 million professional programmers. Various EUD approaches exist, and it is an active research topic within the field of computer science and human-computer interaction. Examples include natural language programming, spreadsheets, scripting languages, visual programming, trigger-action programming and programming by example.

Requirements traceability is a sub-discipline of requirements management within software development and systems engineering. Traceability as a general term is defined by the IEEE Systems and Software Engineering Vocabulary as (1) the degree to which a relationship can be established between two or more products of the development process, especially products having a predecessor-successor or primary-subordinate relationship to one another; (2) the identification and documentation of derivation paths (upward) and allocation or flowdown paths (downward) of work products in the work product hierarchy; (3) the degree to which each element in a software development product establishes its reason for existing; and (4) discernible association among two or more logical entities, such as requirements, system elements, verifications, or tasks.

<span class="mw-page-title-main">Jeannette Wing</span> American computer scientist

Jeannette Marie Wing is Avanessians Director of the Data Science Institute at Columbia University, where she is also a professor of computer science. Until June 30, 2017, she was Corporate Vice President of Microsoft Research with oversight of its core research laboratories around the world and Microsoft Research Connections. Prior to 2013, she was the President's Professor of Computer Science at Carnegie Mellon University, Pittsburgh, Pennsylvania, United States. She also served as assistant director for Computer and Information Science and Engineering at the NSF from 2007 to 2010. She was appointed the Columbia University executive vice president for research in 2021.

ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet.

Ch is a proprietary cross-platform C and C++ interpreter and scripting language environment. It was originally designed by Harry H. Cheng as a scripting language for beginners to learn mathematics, computing, numerical analysis, and programming in C/C++. Ch is now developed and marketed by SoftIntegration, Inc, with multiple versions available, including a freely available student edition and Ch Professional Edition for Raspberry Pi is free for non-commercial use.

<span class="mw-page-title-main">Tachyon (software)</span>

Tachyon is a parallel/multiprocessor ray tracing software. It is a parallel ray tracing library for use on distributed memory parallel computers, shared memory computers, and clusters of workstations. Tachyon implements rendering features such as ambient occlusion lighting, depth-of-field focal blur, shadows, reflections, and others. It was originally developed for the Intel iPSC/860 by John Stone for his M.S. thesis at University of Missouri-Rolla. Tachyon subsequently became a more functional and complete ray tracing engine, and it is now incorporated into a number of other open source software packages such as VMD, and SageMath. Tachyon is released under a permissive license.

<span class="mw-page-title-main">Juan Pavón</span> Spanish computer scientist (b.1962)

Juan Pavón is a Spanish computer scientist, full professor of the Complutense University of Madrid (UCM). He is a pioneer researcher in the field of Software Agents, co-creator of the FIPA MESSAGE and INGENIAS methodologies, and founder and director of the research group GRASIA: GRoup of Agent-based, Social and Interdisciplinary Applications at UCM. He is known for his work in the field of Artificial Intelligence, specifically in agent-oriented software engineering. He has been often cited by mainstream media, as a reference in Artificial Intelligence.

<span class="mw-page-title-main">INGENIAS</span>

INGENIAS is an open-source software framework for the analysis, design and implementation of multi-agent systems (MAS).

<span class="mw-page-title-main">Dlib</span> Cross-platform software library

Dlib is a general purpose cross-platform software library written in the programming language C++. Its design is heavily influenced by ideas from design by contract and component-based software engineering. Thus it is, first and foremost, a set of independent software components. It is open-source software released under a Boost Software License.

EvoSuite is a tool that automatically generates unit tests for Java software. EvoSuite uses an evolutionary algorithm to generate JUnit tests. EvoSuite can be run from the command line, and it also has plugins to integrate it in Maven, IntelliJ and Eclipse. EvoSuite has been used on more than a hundred open-source software and several industrial systems, finding thousands of potential bugs.

Drama annotation is the process of annotating the metadata of a drama. Given a drama expressed in some medium, the process of metadata annotation identifies what are the elements that characterize the drama and annotates such elements in some metadata format. For example, in the sentence "Laertes and Polonius warn Ophelia to stay away from Hamlet." from the text Hamlet, the word "Laertes", which refers to a drama element, namely a character, will be annotated as "Char", taken from some set of metadata. This article addresses the drama annotation projects, with the sets of metadata and annotations proposed in the scientific literature, based markup languages and ontologies.

Communication in Distributed Software Development is an area of study that considers communication processes and their effects when applied to software development in a globally distributed development process. The importance of communication and coordination in software development is widely studied and organizational communication studies these implications at an organizational level. This also applies to a setting where teams and team members work in separate physical locations. The imposed distance introduces new challenges in communication, which is no longer a face to face process, and may also be subjected to other constraints such as teams in opposing time zones with a small overlap in working hours.

References

  1. Smith, Graeme (2000). The Object-Z Specification Language. Springer. ISBN   978-1-4615-5265-9.
  2. Mahony, B.; Dong, Jin Song (February 2000). "Timed Communicating Object Z". IEEE Transactions on Software Engineering . 26 (2): 150–177. CiteSeerX   10.1.1.62.820 . doi:10.1109/32.841115.
  3. Dong, J.S.; Duke, R.; Hao, P. (2005). "Integrating Object-Z with Timed Automata". 10th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'05). Engineering of Complex Computer Systems. pp. 488–497. CiteSeerX   10.1.1.62.793 . doi:10.1109/ICECCS.2005.56. ISBN   978-0-7695-2284-5. S2CID   10062286.
  4. Derrick, John; Boiten, Eerke A. (2014). Refinement in Z and Object-Z (2nd ed.). Springer. ISBN   978-1-4471-5355-9.
Listen to this article (1 minute)
Sound-icon.svg
This audio file was created from a revision of this article dated 19 November 2022 (2022-11-19), and does not reflect subsequent edits.