ajouterCours( c: Cours, sorte: SorteDeCours )
    pre CoursPasDejaPresent:
      cours()->excludes(c)
    pre CoursAppropriePourProgramme:
      self.oclIsTypeOf(Baccalaureat) implies c.numero < 7000

    post CoursObligatoireAjouteSiObligatoire:
      sorte = #Obligatoire implies obligatoires = obligatoires@pre->including(c)
    post CoursAuChoixAjouteSiAuChoix:
      sorte = #AuChoix implies auChoix = auChoix@pre->including(c)

-------------------

  supprimerCours( c: Cours )
    pre CoursPresent:
      cours()->includes(c)

    post UnCoursDeMoins:
      let nbCoursAvant: Integer = obligatoires@pre->union(auChoix@pre)->size() in
        cours()->size() = nbCoursAvant - 1
    post CoursSupprime:
      cours()->excludes(c)

-------------------

  creerCours( sigle: Sigle, titre: String, numero: Integer, nbCredits: Integer, prealables: Set(Cours) ): Cours
    pre NumeroPositif:
       0 < numero and numero <= 9999
    pre SigleEtNumeroUnique:
      Cours.allInstances->select( c | c.sigle = sigle and c.numero = numero )
                        ->isEmpty()
    pre NbCreditsNonNegatif:
       nbCredits >= 0
    pre PrealablesOk: 
      prealables->forAll( c | numero >= 7000 = c.estCoursGradue() )

    post NouveauCours:
      result.oclIsNew()
    post AttributsDefinis:
      result.titre = titre
      and
      result.numero = numero
      and 
      result.nbCredits = nbCredits
    post SigleSpecifie: 
      result.sigle = sigle
    post PrealablesSpecifies:
      result.prealables = prealables
    post AjouteDansBanqueDeCours:
      banqueDeCours = banqueDeCours@pre->including(result)

-------------------

   creerMaitrise( nom: String, nbCredits: Integer, 
                  obligatoires: Set(Cours), auChoix: Set(Cours)
                 ): Maitrise
     pre NbCreditsPositifEtValide:
       nbCredits > 0 
       and
       nbCredits >= obligatoires.nbCredits->sum() + auChoix.nbCredits->sum()
     pre TousGradues:
       obligatoires->union( auChoix )->forAll( numero >= 7000 )
     pre DansBanqueDeCoursDuDepartement:
       banqueDeCours->includesAll( obligatoires->union( auChoix ) )
     pre ObligatoiresPasAuChoix:
       obligatoires->intersection( auChoix )->isEmpty()

     post NouveauProgramme:
       result.oclIsNew()
     post AttributsDefinis:
       result.nbCredits = nbCredits
       and
       result.nom = nom
     post NumeroNouveauEtDistinct:
       Programme.allInstances@pre->forAll( numero <> result.numero )
     post ObligatoiresDefinis:
       result.obligatoires = obligatoires
     post AuChoixDefinis:
       result.auChoix = auChoix
     post DansProgrammes:
       programmes = programmes@pre->including(result)