192 10. PREDICATES AND PROGRAMMING Exercises on program specifications 10.6 Form

Question

192 10. PREDICATES AND PROGRAMMING Exercises on program specifications 10.6 Formalize the following English specifications. Be sure to introdiros essary restrictions. Also, if there are ambiguities or vague parts of the specification, resolve them in some reasonable way (there may not be a answer). You may use x y for the maximum of x and y . Note that is syn metric and associative, so can be used as a quantifier (see Chap. 8). Howeve over the integers has no identity, so axioms that require an identity cannot be used with it. introduce te sing a) Calculate the sum of the elements of blj.k 1]. (b) Find the maximum value of b[..k-1] . (C) Find the index of a maximurn value of bl..k-1] d) Store in array c[O.n 1] a sorted (in ascending order) permutation. mutation o 60.-1]. Use the predicate perm(b, c, n) to denote that bO.n permutation of co.n-1] (see Exercise 10.2). You can also use P ascending(b, n) of Exercise 10.3. Calculate the greatest power of 2 that is not greater t Iso use predicate han n. (f) Count how many zeros b0..n (g) Suppose we have an arrar int 1] has. ents ents bi J

Explanation / Answer

b)

  

c)

predicate maximum_arg(array[int] of var int: x, var int: i) =
let {
int: l = min(index_set(x)),
int: u = max(index_set(x)),
int: ly = lb_array(x),
int: uy = ub_array(x),
array[l..u] of var ly..uy: y,
array[l..u] of var l..u: mi,
} in (
y[l]==x[l] / mi[l]==l /
i==mi[u] /
forall ( j in l+1..u ) (
y[j]==max(x[j], y[j-1]) /
mi[j]==if y[j-1]>=x[j] then mi[j-1] else j endif
))

d)

Related Questions

Navigate

• Browse (All)
• Browse 1
• Subjects

---

---

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.