71 lines
2.1 KiB
Ada
Executable file
71 lines
2.1 KiB
Ada
Executable file
-- Spécification d'un module Dates très simplifié.
|
|
--
|
|
-- Attention : Bien gérer les dates est compliqué. Les dates et opérations
|
|
-- associées sont disponibles dans les bibliothèques des langages de
|
|
-- programmation. Par exemple dans le paquetage Ada.Calendar pour Ada.
|
|
|
|
package Dates is
|
|
|
|
type T_Mois is (JANVIER, FEVRIER, MARS, AVRIL, MAI, JUIN, JUILLET,
|
|
AOUT, SEPTEMBRE, OCTOBRE, NOVEMBRE, DECEMBRE);
|
|
|
|
type T_Date is private;
|
|
|
|
-- Initialiser une date à partir du jour, du mois et de l'année.
|
|
--
|
|
-- Paramètres :
|
|
-- Date : la date à initialiser
|
|
-- Jour : la valeur du jour
|
|
-- Mois : la valeur du mois
|
|
-- Annee : la valeur de l'année
|
|
--
|
|
-- Nécessite :
|
|
-- Jour/Mois/Annee constituent une date valide
|
|
--
|
|
-- Assure
|
|
-- Le_Jour (Date) = Jour
|
|
-- Le_Mois (Date) = Mois
|
|
-- L_Annee (Date) = Annee
|
|
--
|
|
procedure Initialiser ( Date : out T_Date ;
|
|
Jour : in Integer ;
|
|
Mois : in T_Mois ;
|
|
Annee : in Integer )
|
|
with
|
|
Pre => Annee >= 0 and Jour >= 1 and Jour <= 31, -- simplifiée !
|
|
Post => Le_Jour (Date) = Jour and Le_Mois (Date) = Mois and L_Annee (Date) = Annee;
|
|
|
|
-- Afficher une date sous la forme jj/mm/aaaa
|
|
procedure Afficher (Date : in T_Date);
|
|
|
|
-- Obtenir le mois d'une date.
|
|
-- Paramètres
|
|
-- Date : la date dont on veut obtenir le moi
|
|
function Le_Mois (Date : in T_Date) return T_Mois;
|
|
|
|
-- Obtenir le jour d'une date.
|
|
-- Paramètres
|
|
-- Date : la date dont on veut obtenir le jour
|
|
function Le_Jour (Date : in T_Date) return Integer;
|
|
|
|
-- Obtenir l'année d'une date.
|
|
-- Paramètres
|
|
-- Date : la date dont on veut obtenir l'année
|
|
function L_Annee (Date : in T_Date) return Integer;
|
|
|
|
|
|
private
|
|
|
|
type T_Date is
|
|
record
|
|
Jour : Integer;
|
|
Mois : T_Mois;
|
|
Annee : Integer;
|
|
-- Invariant
|
|
-- Annee > 0
|
|
-- Jour >= 1
|
|
-- Jour <= Nombre_Jours (Mois, Annee)
|
|
end record;
|
|
|
|
end Dates;
|