Add properties to Text.Encodings.Base64

src/libraries/OS-Independent/Text/Encodings/Base64.dcl

 definition module Text.Encodings.Base64
 
-/*
+/**
  * Base64 and Base64URL encoding/decoding according to RFC4648. More info:
  * - http://tools.ietf.org/html/rfc4648
  * - http://en.wikipedia.org/wiki/Base64
+ *
+ * @property-bootstrap
+ *   import StdEnv
+ *   import Text
  */
  
 :: Length :== Int
@@ -13,21 +17,33 @@ definition module Text.Encodings.Base64
  
 /**
  * Converts a String to a Base64-encoded String.
+ * @property inverse: A.x :: String:
+ *   base64Decode (base64Encode x) == x
  */
 base64Encode :: !.String -> .String
 
 /**
  * Converts a String to a Base64-encoded String given a maximum line length.
+ * @property inverse: A.len :: Int; x :: String:
+ *   len > 0 ==> base64Decode (base64EncodeLen x len) == x
+ * @property max length: A.len :: Int; x :: String:
+ *   len > 0 ==> all ((>=) len o size) (split "\n" (base64EncodeLen x len))
  */
 base64EncodeLen :: !.String !Length -> .String
 
 /**
  * Converts a String to an URL-safe Base64-encoded String.
+ * @property inverse: A.x :: String:
+ *   base64URLDecode (base64URLEncode x) == x
  */
 base64URLEncode :: !.String -> .String
 
 /**
  * Converts a String to an URL-safe Base64-encoded String given a maximum line length.
+ * @property inverse: A.len :: Int; x :: String:
+ *   len > 0 ==> base64URLDecode (base64URLEncodeLen x len) == x
+ * @property max length: A.len :: Int; x :: String:
+ *   len > 0 ==> all ((>=) len o size) (split "\n" (base64URLEncodeLen x len))
  */
 base64URLEncodeLen :: !.String !Length -> .String