diff --git a/src/fs-filo-vfs.ads b/src/fs-filo-vfs.ads
index 7e756d7..7a2aabb 100644
--- a/src/fs-filo-vfs.ads
+++ b/src/fs-filo-vfs.ads
@@ -8,8 +8,8 @@
 
    type T (<>) is private;
 
-   with function Is_Mounted (State : T) return Boolean;
-   with function Is_Open (State : T) return Boolean
+   with function Is_Mounted (State : T) return Boolean is <>;
+   with function Is_Open (State : T) return Boolean is <>
    with
       Post => (if Is_Open'Result then Is_Mounted (State));
 
@@ -19,6 +19,7 @@
      (State    : in out T;
       Part_Len : in     Partition_Length;
       Success  :    out Boolean)
+   is <>
    with
       Pre => not Is_Mounted (State),
       Post => Success = Is_Mounted (State);
@@ -28,11 +29,13 @@
       File_Len    :    out File_Length;
       File_Path   : in     String;
       Success     : out    Boolean)
+   is <>
    with
       Pre => Is_Mounted (State) and not Is_Open (State),
       Post => Success = Is_Open (State);
 
    with procedure Close (State : in out T)
+   is <>
    with
       Pre => Is_Open (State),
       Post => Is_Mounted (State);
@@ -43,6 +46,7 @@
       File_Pos : in out File_Offset;
       Buf      :    out Buffer_Type;
       Len      :    out Natural)
+   is <>
    with
       Pre => Is_Open (State),
       Post => Is_Open (State);