  Estimating the effort and quality of a system is a critical step at the
beginning of every software project. It is necessary to have reliable ways of
calculating these measures, and, it is even better when the calculation can be
done as early as possible in the development life-cycle.
  Having this in mind, metrics for formal specifications are examined with a
view to correlations to complexity and quality-based code measures. A case
study, based on a Z specification and its implementation in ADA, analyzes the
practicability of these metrics as predictors.
