Feedback on paper of Renker & Ahriz.


METHODOLOGY

The paper has a single composite claim, which is clearly stated in the abstract:

	"... the already existing Z notation, although not previously used in
	this context, proves to a high degree expressive, adaptable, and useful
	for the construction of [constraint and optimisation] problem models."

Additionally, the abstract asserts that no new modelling language is required,
since Z is especially well suited to the task.

The abstract also contains the evaluation plan:

	"To substantiate these claims, we have both compiled a large number of
	constraint and optimisation problems as formal Z specifications and
	translated models from a variety of constraint languages into Z."

Unfortunately, only one of these example problem specifications is described (in
section 4). The others "are available as an online library of model
specifications, which we make openly available to the modelling
community". Unfortunately, as several of you pointed out, the url for these
models is now stale, so the key evidence for a paper only 5 years old is
unavailable.



FLAWS

Since only one example is described, the paper is not self-contained. It must be
read in concert with the "more than 50 online examples" to provide sufficient
evidence of the claims. More importantly, the use of Z is described as
"successful" in the conclusion. But we are not given any way of assessing
success, so we can't verify this claim. We might, for instance, have been
provided with the following kinds of evidence:

* A discussion of the expressivity, adaptability and/or usefulness of the Z
models, as claimed in the main claim above. 

* Z specifications are usually used to verify some properties of an
implementation. Such a use is envisaged as the "third aspect" on p396, but no
such verification proof is given.

There is no comparison with related work. In particular, no justification is
given as to why Z is chosen over its rival.


YOUR REVIEWS

Z is one of the most popular formalisms for formal specification of software and
hardware, and is in widespread use in academia and industry. Section 2 of the
paper is included as background on Z to make the paper self-contained for
readers not familiar with this standard work. The paper contains many generic
statements about the advantages and uses of formal specification. Some of you
interpreted these statements, wrongly, as novel claims about the work
described. Be careful to distinguish such background material from the novel
contributions of a paper.

Some of you missed the key criticism that no success criteria were given for the
modelling results.  An author should always make clear the grounds on which
success is to be judged. Sometimes this is given implicitly in the comparisons
with related work, which is why the omission of this section from the paper is
such a significant flaw.