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)
        ans = 0 - x
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (ans == (0 - x))
        # (x < 0)
        # (x != 0)
        #PREMISES FOR NEXT LINE: 
        # (ans == (0 - x))
        # (x < 0)
        # (x != 0)
    else :
        #PREMISES FOR ELSE-ARM: 
        # not (x < 0)
        # (x != 0)
        ans = x
        #PREMISES FOR ATTACHED PROOF, IF ANY: 
        # (ans == x)
        # not (x < 0)
        # (x != 0)
        #PREMISES FOR NEXT LINE: 
        # (ans == x)
        # not (x < 0)
        # (x != 0)
    #PREMISES FOR NEXT LINE: 
    # (((ans == (0 - x)) and (x < 0)) or ((ans == x) and not (x < 0)))
    # (x != 0)
    return ans
    #PREMISES FOR NEXT LINE: 
    # (((ans == (0 - x)) and (x < 0)) or ((ans == x) and not (x < 0)))
    # (x != 0)
    # (ans > 0)
#PREMISES FOR NEXT LINE: