001package components.stopwatch;
002
003import components.standard.Standard;
004
005/**
006 * Stopwatch component with all its methods. (Note: by package-wide convention,
007 * all references are non-null.)
008 *
009 * @mathsubtypes <pre>
010 * STOPWATCH_MODEL is (
011 *   time: integer,
012 *   running: boolean
013 *  )
014 *  exemplar s
015 *  constraint
016 *   s.time = [CPU time in milliseconds that this.running has been true]
017 * </pre>
018 * @mathmodel type Stopwatch is modeled by STOPWATCH_MODEL
019 * @initially <pre>
020 * ():
021 *  ensures
022 *   this = (0, false)
023 * </pre>
024 */
025public interface Stopwatch extends Standard<Stopwatch> {
026
027    /**
028     * Starts {@code this}.
029     *
030     * @updates this.running
031     * @requires not this.running
032     * @ensures this.running
033     */
034    void start();
035
036    /**
037     * Stops {@code this}.
038     *
039     * @updates this.running
040     * @requires this.running
041     * @ensures not this.running
042     */
043    void stop();
044
045    /**
046     * Returns {@code this.time} in milliseconds.
047     *
048     * @return {@code this.time}
049     * @ensures elapsed = this.time
050     */
051    int elapsed();
052
053    /**
054     * Returns {@code this.running}.
055     *
056     * @return {@code this.running}
057     * @ensures isRunning = this.running
058     */
059    boolean isRunning();
060
061}