China
Africa
Explore chapters and articles related to this topic
A
Published in Phillip A. Laplante, Dictionary of Computer Science, Engineering, and Technology, 2017
(3) any business rule that is a constraint on the property values of an object. Assertions may be one of three kinds: a pre-condition is any assertion that must hold before the execution of an associated operation(s); a post-condition is any assertion that must hold after the execution of the associated operation(s); and a (class) invariant is any assertion that must hold both before and after the execution of all operations. In logic programming, an assertion can be a logic expression specifying a program feature or a set of features that a program/system has to present. See also invariant, proof of correctness.
Formal Methods
Published in Janet Woodcock, Software Engineering Mathematics, 1988
In VDM, an operation is specified by providing an explicit precondition, and an explicit postcondition. The precondition is of course a predicate on the state before the operation. The postcondition'' is a predicate on the state before and the state after the operation. Splitting the relation describing the state transition into two parts is regarded as a good discipline in VDM: it highlights the distinction between the assumption that an implementor is allowed to make, and the obligation that must be met. It also leads to some pleasing formulations of the proof obligations themselves.
Eiffel: A Language for Object-Oriented Software Engineering
Published in Paul W. Ross, The Handbook of Software for Engineers and Scientists, 2018
The most unique aspect of Eiffel is shown within the clauses marked ‘require’ and ‘ensure.’ The boolean statements within these clauses are the “preconditions” and “postconditions” of the routines and are forms of Eiffel assertions. (Class invariants, loop invariants, loop variants, and general checks are also supported.) The preconditions require that provided arguments are acceptable and that the object is in the proper state for handling the feature call. Postconditions ensure that a feature performed correctly and left the object in a correct state.
From strong to exact Petri net computers
Published in International Journal of Parallel, Emergent and Distributed Systems, 2022
Dmitry A. Zaitsev, MengChu Zhou
In order not to handle two variants of a net, we only mention transformations applied to the source Esparza's net [12] and justify the obtained constructs independently. To be mentioned, we merge sequences of transitions which increment/decrement a few variables into a single transition. In and , we replace a loop that checks a postcondition by a loop that checks a precondition and merge two subnets and into a single subnet with two switching places and .
Copy and remove as dynamic operators
Published in Journal of Applied Non-Classical Logics, 2021
Carlos Areces, Hans van Ditmarsch, Raul Fervari, Bastien Maubert, François Schwarzentruber
An action model is a tuple , where: E is a non-empty finite set of action points; is a set of relations , with ; is a precondition function; and is an effect function (also known as the postcondition function), such that for every , is the identity function on all but a finite set of propositional symbols, that we write .
Lightweight Intuitive Provenance (LiP) in a distributed computing environment
Published in International Journal of Computers and Applications, 2019
Wolali Ametepe, Changda Wang, Selasi Kwame Ocansey, XiaWei Li
space occupancy: For safety estimation of memory usage, we propose a size-polymorphic type scheme, which sustain an interprocedural size analysis, where the provenance values are directly captured where with the the size variables which define the properties of the size, which are described as an invariant constraint and in the size relation φ. To identify memory consumption, we declare each method with the following where , here , and denote the postcondition and precondition of our space usage method. We capture the memory effect by and , where denotes maximum space consumed and represents maximum space recovered at end of a process. Recovery and consumption in our setup are expressed by where represents class type, presents its symbolic count.