China
Africa
Explore chapters and articles related to this topic
Introduction to Algorithms and Data Structures
Published in Sriraman Sridharan, R. Balakrishnan, Foundations of Discrete Mathematics with Algorithms and Programming, 2019
Sriraman Sridharan, R. Balakrishnan
A loop invariant (or general snapshots or inductive assertion) is an assertion or a relation among variables of a program, which is always true at a given point in the loop, irrespective of the number of executions of the loop performed before. Mathematical induction and program proving are intimately related. To show that a loop gives the desired result on exiting, we use induction on the number of executions of the loop or some sort of induction on the values of an input variable. Invariants hold at particular points of a program text and they can be considered as a “bridge” between the static program text (spread out in text space) and the dynamic process of computation. In fact, the proof of a loop/inductive assertion involves the following three constituents:Initialization: The invariant is true at/before the entry of the loop. (Induction basis)Preservation: The assertion is conserved one execution after another. (Induction leap)Termination/Finiteness : The loop terminates after a finite number of executions.The following example illustrates this idea on Euclid’s algorithm.
A mechanism design framework for hiring experts in e-healthcare
Published in Enterprise Information Systems, 2020
Vikash Kumar Singh, Sajal Mukhopadhyay, Fatos Xhafa
● Maintenance: For the loop invariant to be true, if it is true before each iteration of while loop, it remains true before the next iteration. The body of while loop allocates doctor(s) to the patient(s) with each doctor is allocated to one patient present in the detected cycle; each time is incremented or each time n is decremented by . Just before the iteration the number of patient–doctor pairs allocated are , implies that the number of patient–doctor pairs left are: . After the iteration, two cases may arise:
Conflict Detection among Multiple Norms in Multi-Agent Systems
Published in Applied Artificial Intelligence, 2018
Eduardo Augusto Silvestre, Viviane Torres da Silva
To prove the correctness of algorithms that have loop, one must use the loop invariants in the proof. In JML, a loop specification consists of the following parts: the keyword loop_invariant (specifies a loop invariant), the keyword decreasing (specifies a value which is always positive and strictly decreased in each loop iteration; it is used to prove termination of the loop) and the keyword assignable/modifies (limits the locations that may be changed by the loop).