class Heure:
    def __init__(self, heures = 0, minutes = 0):
        assert heures >= 0 and minutes >= 0
        self.heures = heures
        self.minutes = minutes
        self.invariant()

    def incrementer(self):
        self.invariant()
        self.minutes = self.minutes + 1
        self.invariant()

    def incrementer2(self):
        self.invariant()
        if (self.minutes < 59):
            self.minutes = self.minutes+1
        else:
            self.minutes = 0
            if self.heures < 23:
                self.heures = self.heures + 1
            else:
                self.heures = 0
        self.invariant()

    def invariant(self):
        assert self.heures >= 0 and self.heures < 24
        assert self.minutes >= 0 and self.minutes < 60

#Preuve init
#    (heures >= 0 and minutes >= 0) => [self.heures = heures || self.minutes = minute](
#        self.heures >= 0 and self.heures < 24 and self.minutes >= 0 and self.minutes < 60)
#    Soit :
#    (heures >= 0 and minutes >= 0) =>(heures >= 0 and heures < 24 and minutes >= 0 and minutes < 60)


#Preuve incrémenter
#    (self.heures >= 0 and self.heures < 24 and self.minutes >= 0 and self.minutes < 60) =>
#        [self.minutes = self.minutes + 1](self.heures >= 0 and self.heures < 24 and self.minutes >= 0 and self.minutes < 60)
#    Soit :
#    (self.heures >= 0 and self.minutes >= 0 and self.minutes >= 0 and self.minutes < 60) => (
#         self.heures >= 0 and
#         self.heures < 24 and
#         self.minutes+1 >= 0 and
#         self.minutes < 60)

#Solution précondition : ajouter assert self.minutes <= 58
#    (self.heures >= 0 and self.heures < 24 and self.minutes >= 0 and self.minutes < 60 and self.minutes <= 58) =>
#        [self.minutes = self.minutes + 1](self.heures >= 0 and self.heures < 24 and self.minutes >= 0 and self.minutes < 60)
#    Soit :
#    (self.heures >= 0 and self.minutes >= 0 and self.minutes >= 0 and self.minutes < 60 and self.minutes <= 58) => (
#         self.heures >= 0 and
#         self.heures < 24 and
#         self.minutes+1 >= 0 and
#         self.minutes < 60)

#Solution améliorée avec incrémenter2
#    Faire 3 cas