def absValue(x) :
    """{ pre  x != 0
         post ans > 0
         return ans
    }"""
    #PREMISES FOR NEXT LINE: 
    # (x != 0)
    if x < 0 :
        #PREMISES FOR THEN-ARM: 
        # (x < 0)
        # (x != 0)
        """{ 1.OK x != 0    premise
             2.OK x < 0     premise
        }"""
        #PREMISES FOR NEXT LINE: 
        # (x < 0)
        ans = 0 - x
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (ans == (0 - x))
        # (x < 0)
        """{ 1.OK x < 0         premise
             2.OK ans == 0 - x  premise
             3.OK ans > 0       algebra 1 2
        }"""
        #PREMISES FOR NEXT LINE: 
        # (ans > 0)
    else :
        #PREMISES FOR ELSE-ARM: 
        # not (x < 0)
        # (x != 0)
        """{ 1.OK x != 0       premise
             2.OK not(x < 0)   premise
             3.OK x >= 0       algebra 2
             4.OK x > 0        algebra 1 3
        }"""
        #PREMISES FOR NEXT LINE: 
        # (x > 0)
        ans = x
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (ans == x)
        # (x > 0)
        """{ 1.OK  ans == x   premise
             2.OK  x > 0      premise
             3.OK  ans > 0    subst 1 2
        }"""
        #PREMISES FOR NEXT LINE: 
        # (ans > 0)
    #PREMISES FOR NEXT LINE: 
    # (ans > 0)
    # (x != 0)
    """{ 1.OK  ans > 0         premise   }"""  
    #PREMISES FOR NEXT LINE: 
    # (ans > 0)
    # that is, we proved (ans > 0  or  ans > 0), which is  ans > 0
    return ans
    #PREMISES FOR NEXT LINE: 
    # (ans > 0)
#PREMISES FOR NEXT LINE: 
    # we proved the postcondition