Overview | Package | Class | Tree | Deprecated | Index | Help
| SOA © 2004 SoS Group All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## sos.koa
Class CandidateListMetadata

    java.lang.Object
      sos.koa.CandidateListMetadata

class CandidateListMetadata
extends java.lang.Object

The metadata associated with a candidiate list for an election.

Version:
  $Id: CandidateListMetadata.java,v 1.12 2004/05/04 19:51:51 martijno Exp $
Author:
  Joe Kiniry (kiniry@cs.kun.nl)

Class Specifications
invariant 0 <= my_kiesKringCount; invariant my_kiesKringCount <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST; invariant 0 <= my_districtCount; invariant my_districtCount <= KiesKring.MAX_DISTRICTS_PER_KIESKRING; invariant 0 <= my_kiesLijstCount; invariant my_kiesLijstCount <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING; invariant 0 <= my_positieCount; invariant 0 <= my_codeCount;

Field Summary
`[spec_public] private int` | `my_codeCount` The number of candidate codes contained in the associated candidate list.
`[spec_public] private java.lang.String` | `my_creationTime` The creation time of the associated candidate list.
`[spec_public] private int` | `my_districtCount` The number of districts in the associated candidate list.
`[spec_public] private byte` | `my_kiesKringCount` The number of kieskringen in the associated candidate list.
`[spec_public] private byte` | `my_kiesLijstCount` The number of kieslijsten in the associated candidate list.
`[spec_public] private int` | `my_positieCount` The total number of candidates in the associated candidate list.
`[spec_public] private java.lang.String` | `my_requestReference` The request reference of the associated candidate list.
`[spec_public] private java.lang.String` | `my_responseReference` The response reference of the associated candidate list.

Constructor Summary
`(package private)` | `CandidateListMetadata(non_null java.lang.String a_request_reference, non_null java.lang.String a_response_reference, non_null java.lang.String a_creation_time, byte a_kieskring_count, int a_district_count, byte a_kieslijst_count, int a_positie_count, int a_code_count)` Construct a new candidate list metadata object given the specified initialization values.

Method Summary
`(package private) int` | `codeCount()`
`(package private) java.lang.String` | `creationTime()`
`(package private) int` | `districtCount()`
`(package private) byte` | `kiesKringCount()`
`(package private) byte` | `kiesLijstCount()`
`(package private) int` | `positieCount()`
`(package private) java.lang.String` | `requestReference()`
`(package private) java.lang.String` | `responseReference()`
`java.lang.String` | `toString()` {@inheritDoc}

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`

Field Detail

### my_requestReference

    private java.lang.String my_requestReference

  The request reference of the associated candidate list.

  Specifications: spec_public non_null

### my_responseReference

    private java.lang.String my_responseReference

  The response reference of the associated candidate list.

  Specifications: spec_public non_null

### my_creationTime

    private java.lang.String my_creationTime

  The creation time of the associated candidate list.

  Specifications: spec_public non_null

### my_kiesKringCount

    private byte my_kiesKringCount

  The number of kieskringen in the associated candidate list.

  Specifications: spec_public

### my_districtCount

    private int my_districtCount

  The number of districts in the associated candidate list.

  Specifications: spec_public

### my_kiesLijstCount

    private byte my_kiesLijstCount

  The number of kieslijsten in the associated candidate list.

  Specifications: spec_public

### my_positieCount

    private int my_positieCount

  The total number of candidates in the associated candidate list.

  Specifications: spec_public

### my_codeCount

    private int my_codeCount

  The number of candidate codes contained in the associated candidate list.

  Specifications: spec_public

Constructor Detail

### CandidateListMetadata

    CandidateListMetadata(non_null java.lang.String a_request_reference,
                          non_null java.lang.String a_response_reference,
                          non_null java.lang.String a_creation_time,
                          byte a_kieskring_count,
                          int a_district_count,
                          byte a_kieslijst_count,
                          int a_positie_count,
                          int a_code_count)

  Construct a new candidate list metadata object given the specified initialization values.

  Parameters:
    `a_request_reference` - the request reference of the associated candidate list.
    `a_response_reference` - the response reference of the associated candidate list.
    `a_creation_time` - the creation time of the associated candidate list.
    `a_kieskring_count` - the number of kieskringen in the associated candidate list.
    `a_district_count` - the number of districts in the associated candidate list.
    `a_kieslijst_count` - the number of kieslijsten in the associated candidate list.
    `a_positie_count` - the total number of candidates in the associated candidate list.
    `a_code_count` - the number of candidate codes contained in the associated candidate list.
  See Also:
    `

    `
  Specifications: pure
    normal_behavior
    requires 0 <= a_kieskring_count;
    requires a_kieskring_count <= CandidateList.MAX_KIESKRINGEN_PER_CANDIDATE_LIST;
    requires 0 <= a_district_count;
    requires a_district_count <= KiesKring.MAX_DISTRICTS_PER_KIESKRING;
    requires 0 <= a_kieslijst_count;
    requires a_kieslijst_count <= KiesKring.MAX_KIESLIJSTEN_PER_KIESKRING;
    requires 0 <= a_positie_count;
    requires a_positie_count <= KiesLijst.MAX_CANDIDATES_PER_KIESLIJST*a_kieslijst_count;
    requires 0 <= a_code_count;
    ensures requestReference().equals(a_request_reference);
    ensures responseReference().equals(a_response_reference);
    ensures creationTime().equals(a_creation_time);
    ensures kiesKringCount() == a_kieskring_count;
    ensures districtCount() == a_district_count;
    ensures kiesLijstCount() == a_kieslijst_count;
    ensures positieCount() == a_positie_count;
    ensures codeCount() == a_code_count;

Method Detail

### requestReference

    final java.lang.String requestReference()

  Returns:
    the request reference of the associated candidate list.
  Specifications: pure non_null

### responseReference

    final java.lang.String responseReference()

  Returns:
    the response reference of the associated candidate list.
  Specifications: pure non_null

### creationTime

    final java.lang.String creationTime()

  Returns:
    the creation time of the associated candidate list.
  Specifications: pure non_null

### kiesKringCount

    final byte kiesKringCount()

  Returns:
    the number of kieskringen in the associated candidate list.

  Specifications: pure
    normal_behavior
    ensures \result >= 0;

### districtCount

    final int districtCount()

  Returns:
    the number of districts in the associated candidate list.

  Specifications: pure
    normal_behavior
    ensures \result >= 0;

### kiesLijstCount

    final byte kiesLijstCount()

  Returns:
    the number of kieslijst in the associated candidate list.

  Specifications: pure
    normal_behavior
    ensures \result >= 0;

### positieCount

    final int positieCount()

  Returns:
    the total number of candidates in the associated candidate list.

  Specifications: pure
    normal_behavior
    ensures \result >= 0;

### codeCount

    final int codeCount()

  Returns:
    the number of candidate codes in the associated candidate list.

  Specifications: pure
    normal_behavior
    ensures \result >= 0;

### toString

    public final java.lang.String toString()

  {@inheritDoc}

  Overrides:
    `toString` in class `java.lang.Object`

Overview | Package | Class | Tree | Deprecated | Index | Help
| SOA © 2004 SoS Group All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD