Morgan's Calculator

June 22, 2010 – 6 years, 9 months ago, by Vladimir Klebanov

Short Description

A calculator object is able to receive an arbitrary number or real
numbers, and is able to provide to arithmetic mean of the numbers
entered so far.

Long Description

The calculator has the following Java interface:

interface CalcInt {
  // resets the calculator
  void reset();

  // add element x to calculator
  void add(double x);

  // returns the mean of numbers added so far
  double mean();


Problem 1: how could we formally specify this interface?

An implementation can be clever: it only needs to store the sum and the
count of numbers received, e.g the following Java implementation :

class Calculator implements CalcInt {
  private double sum;
  private int count;

  void reset() { sum = 0.0; count = 0; }
  void add(double x) { sum += x; count++; }
  double mean() { return sum/count; }


Problem 2: how to prove it implements the calculator correctly?

Supplementary Materials

This is an example from Carroll Morgan's book ``Programming from
Specifications'', Section 17.6

Subbmitted by

Claude Marché