Skip to Main Content
Requirements Engineering for Software and Systems
book

Requirements Engineering for Software and Systems

by Phillip A. Laplante
March 2011
Intermediate to advanced content levelIntermediate to advanced
264 pages
7h 40m
English
CRC Press
Content preview from Requirements Engineering for Software and Systems
Formal Methods 133
n(n + 1)/2. erefore, upon continued execution of the system, sum will result in
(n + 1) + n(n + 1)/2, which is just (n + 1)(n + 1 + 1)/2 and the system is partially
correct.
Since by the induction hypothesis, by the nth iteration of the loop count has
been decremented n times (since the loop exited when count was initialized to n).
In the induction step, count was initialized to n + 1, so by the nth iteration it has a
value or 1. So after the n + 1st iteration it will be decremented to 0, and hence the
system exits from the loop and terminates.
Does this approach really prove correctness? It does, but if you don’t believe
it, try using Hoare logic to prove an incorrect specification segment to be correct,
for example:
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Start your free trial

You might also like

System Requirements Engineering

System Requirements Engineering

Jean-Yves Bron
Process for System Architecture and Requirements Engineering

Process for System Architecture and Requirements Engineering

Derek Hatley, Peter Hruschka, Imtiaz Pirbhai

Publisher Resources

ISBN: 9781420064681