Let Count be a specification with a single variable n whose behavior specification allows the single infinite behavior
[n = 1] -> [n = 2] -> [n = 3] -> [n = 4] -> ...
Show that if A is any specification whose behavior specification allows an infinite behavior, then Count implements A under some refinement mapping.
A refinement mapping from a specification H to a specification A is an assignment of an expression v to each variable v of A, where v is defined in terms of the variables of H.
Let s1 -> s2 -> s3 -> ... be an infinite behavior satisfying A's behavior specification. For any variable v of A, define v to equal ev(n), where ev(i) is the value of v in state si, for any positive integer i.
We say that H implements A ... iff, for each behavior sigma satisfying the behavior specification of H, the behavior sigma satisfies the behavior specification of A.
Dear Charles,
As a side note, the definition of what it means for H to implement A
reads (in part):
We say that H implements A ... iff, for each behavior sigma
satisfying the behavior specification of H, the behavior sigma
satisfies the behavior specification of A.
Is it correct to read that as (roughly):
\A sigma \in the_set_of_all_behaviors :
sigma satisfies H <=> sigma satisfies A
No, it is not. I will explain why not, and I would appreciate
knowing why you missed what I regard to be the correct interpretation
of that sentence. The parsing of the sentence is
(We say that H implements A ...) iff
(for each behavior sigma satisfying the behavior specification
of H, the behavior sigma satisfies the behavior specification of A.)
The clause (for each ... of A.) is of the form
for every s satisfying A: s satisfies B
which means
\A s : (s satisfies A) => (s satisfies B)
Hence, the correct interpretation is
\A sigma \in the_set_of_all_behaviors : sigma satisfies H => sigma satisfies A
with => rather than <=> .
I believe that any mathematician would interpret the sentence this
way. However, mathematicians tend to assume that their particular
literary style is unambiguously rigorous and don't appreciate how what
they write can be understood differently by intelligent people who are not
familiar with that literary style. So, I would appreciate knowing
what led to your interpretation so I can learn how to write more
clearly for non-mathematicians.
Thanks,
Leslie