Add math package (#6)

math.gobra

@@ -0,0 +1,58 @@
+// This package defines mathematical operations commonly used in specifications.
+package math
+
+ghost
+decreases
+pure func Max(x, y int) int {
+	return x > y ? x : y
+}
+
+ghost
+decreases
+pure func Max3(x, y, z int) int {
+	return Max(Max(x, y), z)
+}
+
+ghost
+decreases
+pure func Min(x, y int) int {
+	return x < y ? x : y
+}
+
+ghost
+decreases
+pure func Min3(x, y, z int) int {
+	return Min(Min(x, y), z)
+}
+
+ghost
+decreases
+pure func Abs(x int) int {
+	return x >= 0 ? x : -x
+}
+
+// Pow raises x to the power of e.
+ghost
+requires e >= 0
+decreases e
+pure func Pow(x, e int) int {
+	return e == 0 ? 1 : x * Pow(x, e - 1)
+}
+
+// Pow raises 2 to the power of e.
+ghost
+requires e >= 0
+decreases
+pure func Pow2(e int) int {
+	return Pow(2, e)
+}
+
+// Clips x to the interval [low, high].
+// If x is not in the interval, Clip returns the closest 
+// value in the interval. Otherwise, it returns x.
+ghost
+requires low <= high
+decreases
+pure func Clip(x, low, high int) int {
+	return Min(Max(x, low), high)
+}