io7m
io7m-jvvfs 4.0.1
io7m-jvvfs 4.0.1 Documentation
1
Package Information
1.1
Orientation
1.1.1
Overview
1
The jvvfs package implements a pseudo virtual filesystem abstraction. The package essentially constructs a unified namespace from sets of mounted archives (such as directories, zip files, etc). It is inspired by PhysicsFS but does not contain support for old proprietary/obscure archive formats.
2
When using a filesystem abstraction such as jvvfs, it becomes very easy for application developers to distribute updates. The developer initially distributes the program resources (images, audio, etc) as one or more zip archives. Updates to the program data then consist of zip archives containing only files that have been changed: these new archives are simply mounted over the top of the old ones in the virtual filesystem.
1.1.2
Portability
1
The package is written in pure Java and is expected to work in any environment supporting Java 6.
2
The filesystem abstraction allows developers to access program resources using platform-independent notation. The package is carefully written to ensure that applications access resources consistently across all platforms (including consistency under erroneous conditions).
1.2
Installation
1.2.1
Source compilation
1
The project can be compiled and installed with Maven:
2
$ mvn -C clean install
1.2.2
Maven
1
Regular releases are made to the Central Repository, so it's possible to use the io7m-jvvfs package in your projects with the following Maven dependency:
2
<dependency>
  <groupId>com.io7m.jvvfs</groupId>
  <artifactId>io7m-jvvfs-core</artifactId>
  <version>4.0.1</version>
</dependency>
3
All io7m.com packages use Semantic Versioning [0], which implies that it is always safe to use version ranges with an exclusive upper bound equal to the next major version - the API of the package will not change in a backwards-incompatible manner before the next major version.
1.3
Platform Specific Issues
1
There are currently no known platform-specific issues.
1.4
License
1
All files distributed with the io7m-jvvfs package are placed under the following license: 
Copyright © 2014 <code@io7m.com> http://io7m.com

Permission to use, copy, modify, and/or distribute this software for any
purpose with or without fee is hereby granted, provided that the above
copyright notice and this permission notice appear in all copies.

THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
2
User Manual
2.1
Overview
2.1.1
Filesystem
1
The jvvfs package presents a virtual filesystem in which archives are mounted to form a unified namespace. This filesystem is conceptually and practically distinct from the filesystem presented by the operating system. The jvvfs package never writes to or otherwise modifies the operating system filesystem in any way.
2
The jvvfs virtual filesystem presents a hierarchical directory system very similar to the typical UNIX filesystem, supporting a subset of the normal UNIX filesystem operations such as retrieving the modification time of a file, retrieving the size of a file in bytes, listing the contents of a directory, and opening a file as a stream of bytes.
2.1.2
Archives
1
An archive is a file or directory in the operating system that can be mounted. The jvvfs package currently supports mounting operating system directories and zip [1] files.
2.1.3
Mounting
1
Mounting an archive makes the contents of that archive accessible in the filesystem.
2
If an archive is mounted at a directory /M, and the archive contains a file or directory named F, then that file or directory is accessible in the virtual filesystem at /M/F. As mentioned, directories can be arbitrarily nested, and archives can be mounted at any directory in the filesystem.
2.1.4
Capabilities
1
The set of operations that can be performed on the virtual filesystem is divided into capabilities. The purpose of this is to allow code to be separated according to the principle of least privilege. That is, if a given function only needs to read from the filesystem and does not need to be able to mount or unmount archives, then it can be declared as taking a value of type FSCapabilityRead as opposed to, for example, a value of type FilesystemType. This allows the type system to give much stronger guarantees about what a particular function can do to the filesystem.
2
See the JavaDoc documentation for FSCapabilityAll for the definitions of the capabilities.
2.2
Tutorial
1
First, the filesystem is created by specifying an archive directory containing archives (zip files, directories, etc):
2.2.1. Filesystem creation
final PathReal path = new PathReal("/path/to/application/resources");
final FilesystemType fs = Filesystem.makeWithArchiveDirectory(log, path);
2
Then, individual archives can be mounted into the filesystem in much the same way as disks are mounted in the UNIX filesystem. All archives are treated in a read-only manner. The jvvfs package never writes to the filesystem or any archives.
3
Values of type PathReal denote platform-specific paths (and should therefore be given in platform-specific notation). Use of File.separatorChar in the Java standard library is recommended.
4
Assuming archive.zip exists in the specified archive directory, the archive can be mounted in the root directory of the virtual filesystem:
2.2.2. Mounting archives
final PathVirtual mount = PathVirtual.ofString("/");
fs.mountArchive("archive.zip", mount);
5
Values of type PathVirtual denote paths in the virtual filesystem and are given in platform-independent notation. Virtual path components are separated by / and must always begin with a leading / (the paths must always be absolute). The filesystem currently has no concept of a "current working directory", so relative paths have no meaning.
6
Assuming archive.zip contains the file /a/b/c/file.txt, the file can be opened, unsurprisingly, by the path /a/b/c/file.txt:
2.2.3. Opening a file
final PathVirtual path   = PathVirtual.ofString("/a/b/c/file.txt");
final InputStream stream = fs.openFile(path);
7
It is possible to mount archives at directories other than the root. It is possible to create directories in the virtual filesystem with the createDirectory function, if no currently mounted archive provides the desired mount point. Manually created directories are purely virtual constructs; creating a directory via the jvvfs API does not modify the real OS filesystem or any archives.
2.2.4. Creating a directory
// If "archive1.zip" contains "/a/b/file.txt", then "archive2.zip" could, for
// example, be mounted at "/a" or "/a/b".
fs.mount("archive1.zip", PathVirtual.ROOT);
assert fs.isDirectory(PathVirtual.ofString("/a"));
assert fs.isDirectory(PathVirtual.ofString("/a/b"));
fs.mount("archive2.zip", PathVirtual.ofString("/a"));

// Explicitly creating "/c" and mounting "archive2.zip" there is also a possibility.
fs.createDirectory(PathVirtual.ofString("/c"));
assert fs.isDirectory(PathVirtual.ofString("/c"));
fs.mount("archive2.zip", PathVirtual.ofString("/c"));

// Assuming "/xyz/file.txt" exists in "archive2.zip", both of the following will work:
final InputStream s0 = fs.openFile("/a/xyz/file.txt");
final InputStream s1 = fs.openFile("/c/xyz/file.txt");
2.3
The Jvvfs Shell
2.3.1
Overview
1
The jvvfs package includes a simple command-line shell program for manipulating and exploring jvvfs filesystems.
2
The program is distributed as part of the io7m-jvvfs-shell package, with the main program provided in the ShellMain class.
3
The program takes a pair of arguments: The name of a configuration file, and the name of a directory containing archive files.
2.3.2
shell.conf
1
The sole purpose of the configuration file, at present, is to control logging. The jvvfs package uses jlog [2] internally for extremely fine-grained control of logging. All logging controls for jvvfs are given the prefix com.io7m.jvvfs. A trivial configuration file that only logs errors is sufficient for almost all users:
2.3.2.1. Example shell.conf
com.io7m.jvvfs.logs.shell = true
com.io7m.jvvfs.level      = LOG_ERROR
2.3.3
Commands
1
Usage information on shell commands can be obtained from the help command. The shell supports tab-completion [3] for commands.
2
A transcript of an example session showing some of the features of the shell is as follows:
2.3.3.1. Example shell session
jvvfs> 
archives         close            file-list        file-list-long   file-read        file-size        file-time        
help             list-mounts      mkdir            mount            unmount  
        
jvvfs> archives 
complex.zip
encrypted.zip
files1-3.zip
files4-6.zip
io7m-jvvfs.properties
single-file-and-subdir-implicit.zip
single-file-and-subdir.zip
single-file-in-subdir-subdir.zip
single-file.jar
single-file.zip
subdir-shadow.zip
subdir-subdir-shadow.zip
unknown.unknown

jvvfs> mkdir /z
jvvfs> file-list-long /
z/                2013-06-29 14:19:51 +0000 
jvvfs> file-list-long /z

jvvfs> mount files1-3.zip /z
jvvfs> file-list-long /z
file1.txt         2013-05-08 11:35:16 +0000 7
file2.txt         2013-05-08 11:35:20 +0000 7
file3.txt         2013-05-08 11:35:24 +0000 7
jvvfs> file-read /z/file1.txt
File 1

jvvfs> list-mounts 
/z  /tmp/jvvfs/files1-3.zip

jvvfs> mount complex.zip /
jvvfs> list-mounts 
/   /tmp/jvvfs/complex.zip
/z  /tmp/jvvfs/files1-3.zip

jvvfs> file-list-long /
a/                2012-03-15 21:13:12 +0000
b/                2012-03-15 21:13:12 +0000
z/                2013-06-28 22:13:47 +0000

jvvfs> file-list-long /a
a/                2012-03-15 21:13:12 +0000
a1.txt            2012-03-15 21:13:12 +0000 9
a2.txt            2012-03-15 21:13:12 +0000 9
a3.txt            2012-03-15 21:13:12 +0000 9
b/                2012-03-15 21:13:12 +0000
c/                2012-03-15 21:13:12 +0000

jvvfs> mount files4-6.zip /a

jvvfs> file-list-long /a
a/                2012-03-15 21:13:12 +0000 
a1.txt            2012-03-15 21:13:12 +0000 9
a2.txt            2012-03-15 21:13:12 +0000 9
a3.txt            2012-03-15 21:13:12 +0000 9
b/                2012-03-15 21:13:12 +0000 
c/                2012-03-15 21:13:12 +0000 
file4.txt         2013-05-08 11:36:02 +0000 7
file5.txt         2013-05-08 11:36:06 +0000 7
file6.txt         2013-05-08 11:36:10 +0000 7

jvvfs> list-mounts 
/a  /tmp/jvvfs/files4-6.zip
/   /tmp/jvvfs/complex.zip
/z  /tmp/jvvfs/files1-3.zip

jvvfs> close
jvvfs> list-mounts
jvvfs> file-list-long /

jvvfs> mount encrypted.zip /
shell : error : filesystem error: archive 'encrypted.zip' appears to be corrupt - invalid CEN header (encrypted entry)
2.4
Migrating from 2.*.*
2.4.1
FilesystemAPI
1
The API exposed by filesystems changed and was broken up into separate filesystem capabilities. See Capabilities for the details. The only significantly different function is getModificationTime, which replaced modificationTime(). This now uses values of type Calendar, to deal correctly with timezones.
2
Most of the function names have changed in order to statically indicate that the semantics may be subtly different.
2.4.2
Filesystem
1
The Filesystem type is still the main filesystem implementation, but now requires that users use the provided static methods to initialize the filesystem, instead of the now-private constructors.
2.4.3
PathVirtual
1
The constructors of the PathVirtual type are now private and were replaced by ofString. The ofString function is much stricter in what it'll accept as a valid path. The ofStringLax function is more permissive in the syntax that it supports and may be required for directly migrating old code.
2
The semantics of the PathVirtual type have also changed with regard to what is considered to be a parent or ancestor of a path. For example, the root directory is now not considered to have a parent. These changes are unlikely to affect any existing code that uses jvvfs. See virtual path semantics for the precise details.
3
Semantics
3.1
Overview
3.1.1
Specification
1
This section attempts to document the semantics of the jvvfs package. The semantics are given as fragments of code written in the Gallina language of Coq [4].
2
The source to the development is available for type-checking and writing exploratory proofs about the model. Note that the source is not intended to be particularly readable by itself, and is formatted for ease of insertion into this documentation (as opposed to being formatted for easy reading).
3.1.2
Effects
1
Many of the operations described in this specification are effectful. That is, they are computations that will perform some side effect and are therefore not directly expressible in Coq's logic. Effectful operations are expressed here as values of type io. The io F S type is understood to represent a computation that, when executed, will perform some side effect and return a value of type S on success or a value of type F on failure.
3.1.2.1. IO
Inductive io (F S : Type) : Type :=
  | Success : S -> io F S
  | Failure : F -> io F S.
2
The issue of side effects makes it somewhat awkward to describe the consequences of actions, so the reader is (unfortunately) required to use good judgement when reading statements regarding effectful computations. As an example of this problem: "If looking up an object at path p in the filesystem succeeds and produces a reference to a file, then looking up the parent of p must succeed and yield a reference to a directory". This is obviously true given normal operating system filesystem semantics. However, looking up objects in the filesystem is an effectful operation and therefore, the filesystem could theoretically burst into flames and never yield the second reference! The reader is more or less expected to implicitly insert the phrase "assuming that no catastrophic operating system errors occur" before reading any statement regarding effectful computations.
3
The problem could be solved to some extent by specifying an even more abstract model of the filesystem and then stating that the effectful computations adhere to properties stated about this model, but this is certainly not trivial and would probably be of little practical utility.
3.2
Names
3.2.1
Semantics
1
Each object in the jvvfs filesystem has exactly one name.
3.2.1.1. Name type
Axiom name       : Set.
Axiom name_valid : name -> Prop.
3.2.2
Syntax
1
Names of filesystem objects in jvvfs are specifically not allowed to contain:
3.2.2.1. Name restrictions
  • Forward slashes (['/'], ASCII [0x2f]), as this is used as a path separator on UNIX and in jvvfs virtual paths.
  • Backslashes (['\'], ASCII [0x5c]), as this is used as a path separator on Microsoft Windows.
  • A series of two or more dots (['.'], ASCII [0x2e]), as this is a reserved name on UNIX-like platforms.
  • Colons ([':'], ASCII [0x3a]), as these are used to identify "drives" on some operating systems.
  • Null (ASCII [0x0]), as almost no operating systems permit these in file names.
2
Empty strings are also not considered to be valid names.
3.3
Virtual paths
3.3.1
Semantics
1
Virtual paths in jvvfs are conceptually a list of names, with the empty list representing the root.
3.3.1.1. Virtual path type
Definition path_virtual :=
  list {n : name | name_valid n}.

Definition root : path_virtual :=
  nil.
2
A path p0 is an ancestor of p1 iff p0 is a prefix of p1 (that is, the first length p0 elements of p1 are equal to p0), but p0 ≠ p1.
3.3.1.2. Virtual path ancestor
Require Coq.Lists.List.

Definition is_prefix (p0 p1 : path_virtual) :=
  List.firstn (length p0) p1 = p0.

Definition is_ancestor_of (p0 p1 : path_virtual) :=
  p0 <> p1 /\ is_prefix p0 p1.
3
Consequently, a path p0 is the parent of p1 iff p0 is an ancestor of p1 and ∃n. app p0 n = p1 (where app is the standard list append function).
3.3.1.3. Virtual path parent
Require Coq.Lists.List.

Definition is_parent_of (p0 p1 : path_virtual) :=
  is_ancestor_of p0 p1 /\ exists n, app p0 (n :: nil) = p1.
4
Iff p1 is an ancestor of p0, or p0 = p1, the subtraction of p1 from p0 is defined as the removal of the first length p1 elements of p0.
3.3.1.4. Virtual path subtraction
Require Coq.Lists.List.

Definition subtract
  (p0 p1 : path_virtual)
  (_     : is_ancestor_of p1 p0 \/ p0 = p1) :=
  List.skipn (length p1) p0.
5
It naturally follows that it is possible to obtain a list of all ancestors of a path p by successively concatenating the elements of p to the root, minus the last element.
3.3.1.5. Virtual path ancestors
Require Coq.Lists.List.

Fixpoint ancestors_including_self (p : path_virtual) : list path_virtual :=
  cons root (match p with
    | nil       => nil
    | cons y ys => List.map (cons y) (ancestors_including_self ys)
    end).

Definition ancestors (p : path_virtual) : list path_virtual :=
  List.removelast (ancestors_including_self p).
3.3.2
Syntax
1
The concrete syntax of virtual paths is given by the following EBNF [5] grammar:
3.3.2.1. Virtual path EBNF
path = "/" , [ name , ("/" , name)* ] ;
2
Where name represents a valid name.
3.4
Archives
3.4.1
Overview
1
Archives represent on-disk files and directories. They support basic operations such as file lookups and directory listing.
2
From the perspective of the jvvfs filesystem, an archive is an opaque value that returns responses to queries made relative to the directory at which the archive is mounted.
3.4.1.1. Archive type
Axiom archive : Set.
3
The directory at which a given archive is mounted is stored along with the archive and is accessible.
3.4.1.2. Archive mount
Axiom archive_mount : archive -> path_virtual.
3.4.2
Lookup
1
Archives contain files and directories, each of which have unique paths. One of the primitive operations supported by archives is returning a reference to one these filesystem objects when given a path.
2
Archives expose their contents as opaque file references. The jvvfs filesystem does not expose these references to the user, but they are used here to express further properties of archives. As stated, a referenced object must either be a file or a directory.
3.4.2.1. Archive file references
Inductive file_reference :=
  | FSReferenceFile
  | FSReferenceDirectory.
3
Looking up an object in an archive is an effectful computation that will return an optional file reference on success. The function returns None for a path p iff all ancestors of p exist and are directories, but no object exists at p. The function returns Some r iff all ancestors of p exist and are directories and an object exists at p, where r is a reference to the object at p. Otherwise, the function returns an error. Some specific error cases are described below.
3.4.2.2. Archive lookup
Axiom archive_lookup : archive -> path_virtual -> io error_code (option file_reference).
4
If the path p refers to a file in the archive a, then attempting to call archive_lookup on any q where is_ancestor_of p q must clearly fail (because only directories can have children).
3.4.2.3. Archive lookup file parent failure
Axiom archive_lookup_file_ancestor : forall
  (a   : archive)
  (p q : path_virtual),
  is_ancestor_of p q ->
    archive_lookup a p = Success _ _ (Some FSReferenceFile) ->
      archive_lookup a q = Failure _ _ FSErrorNotADirectory.
5
Additionally, if archive_lookup yields a reference to anything for some q, then it must yield a reference to a directory for all p where is_ancestor_of p q.
3.4.2.4. Archive lookup directory ancestor
Axiom archive_lookup_ancestor : forall
  (a   : archive)
  (p q : path_virtual),
  is_ancestor_of p q ->
    (exists r, archive_lookup a q = Success _ _ (Some r)) ->
      archive_lookup a p = Success _ _ (Some FSReferenceDirectory).
3.4.3
Directory Listing
1
The contents of directories within archives may be listed. The archive_directory_list function returns a list of names of direct children of the directory at p, iff p refers to a directory and all ancestors of p are directories. Otherwise, the function returns an error.
3.4.3.1. Archive directory listing
Axiom archive_directory_list : archive -> path_virtual -> io error_code (list name).
3.4.3.2. Archive directory listing file failure
Axiom archive_directory_list_file : forall
  (a : archive)
  (p : path_virtual),
  archive_lookup a p = Success _ _ (Some FSReferenceFile) ->
    archive_directory_list a p = Failure _ _ FSErrorNotADirectory.
3.5
Filesystem
3.5.1
Overview
1
The filesystem maintains a list of archives, and presents an interface that allows archives to be "mounted" and "unmounted" at directories within the filesystem.
3.5.2
Lookup
1
Unlike most operating-system filesystems, the jvvfs filesystem has so-called "union" semantics. The filesystem maintains a list of mounted archives, sorted in order of most-recently mounted - the first archive in the list is the archive that was most recently mounted. In order to look up an object in the filesystem at a given path p, it's first necessary to look up all of the ancestors of p to ensure that they exist and are directories. Looking up an object at p directly means to look up p without looking up any of the ancestors of p. When attempting to look up an object directly in the filesystem at a given path p, each archive a in the list of archives is considered in turn, starting with the most recently mounted first. The lookup procedure takes the following steps:
3.5.2.1. Filesystem union search
  1. If a is mounted at a path m such that is_ancestor_of m p or m = p, then the object at subtract p m is looked up in a, and a is said to have been checked. Otherwise, the next archive in the list is considered.
  2. If a returns a reference to an object, then that object is returned immediately and no further archives are considered. If, in a, an ancestor q of subtract p m is a file, then the file at q is said to be shadowing the contents of the rest of the archives. If shadowing is occuring, and a is not the first archive in the list that has been checked so far, then nothing is returned and no further archives are considered. Otherwise, an error is returned (indicating that q is not a directory).
2
If no archives return an object, then no object exists at p in the filesystem.
3
As mentioned, it's necessary to look up all of the ancestors of p to ensure the correct semantics, so the above procedure is simply applied to all ancestors of p before being applied to p itself. If any ancestor of p turns out not to exist, or not to be a directory, or if an error occurs, the function returns an error.
3.5.2.2. Filesystem union search (Coq)
Require Coq.Arith.Peano_dec.

Axiom ancestor_or_equal : forall (p q : path_virtual),
  {is_ancestor_of p q \/ q = p}+{~is_ancestor_of p q \/ q = p}.

Fixpoint filesystem_lookup_union'
  (archives : list archive)
  (p        : path_virtual)
  (checks   : nat)
: io error_code (option file_reference) :=
  match archives with
  | nil         => Success _ _ None
  | cons a rest =>
    let m := archive_mount a in
      match ancestor_or_equal m p with
      | right _ => filesystem_lookup_union' rest p checks
      | left  H =>
        match archive_lookup a (subtract p m H) with
        | Success None                 => filesystem_lookup_union' rest p (S checks)
        | Success (Some r)             => Success _ _ (Some r)
        | Failure FSErrorNotADirectory =>
          if Peano_dec.eq_nat_dec checks 0
          then Failure _ _ FSErrorNotADirectory
          else Success _ _ None
        | Failure e => Failure _ _ e
        end
      end
  end.

Definition filesystem_lookup_union
  (archives : list archive)
  (p        : path_virtual)
:= filesystem_lookup_union' archives p 0.

Fixpoint filesystem_lookup_ancestors
  (archives : list archive)
  (p_a      : list path_virtual)
: io error_code (option file_reference) :=
  match p_a with
  | nil       => Success _ _ (Some (FSReferenceDirectory))
  | cons q qs =>
    match filesystem_lookup_union archives q with
    | Success None                        => Failure _ _ FSErrorNotADirectory
    | Success (Some FSReferenceFile)      => Failure _ _ FSErrorNotADirectory
    | Success (Some FSReferenceDirectory) => filesystem_lookup_ancestors archives qs
    | Failure e                           => Failure _ _ e
    end
  end.

Definition filesystem_lookup
  (archives : list archive)
  (p        : path_virtual)
: io error_code (option file_reference) :=
  match filesystem_lookup_ancestors archives (ancestors p) with
  | Success _ => filesystem_lookup_union archives p
  | Failure e => Failure _ _ e
  end.
4
The above steps are in contrast to how operating-system filesystems usually behave. Typically, operating systems will take steps analogous to the following (where archives are replaced by disks or disk partitions):
3.5.2.3. Typical OS filesystem search
  1. If a is mounted at a path m such that is_ancestor_of m p or m = p, then the object at subtract p m is looked up in a. Otherwise, the next archive in the list is considered.
  2. If, in a, an ancestor q of subtract p m is not a file, an error is returned (indicating that q is not a directory). If a returns a reference to an object, then that object is returned immediately and no further archives are considered. Otherwise, nothing is returned and no further archives are considered.
3.5.2.4. Typical OS filesystem search (Coq)
Require Coq.Arith.Peano_dec.

Fixpoint filesystem_lookup_typical
  (archives : list archive)
  (p        : path_virtual)
: io error_code (option file_reference) :=
  match archives with
  | nil         => Success _ _ None
  | cons a rest =>
    let m := archive_mount a in
      match ancestor_or_equal m p with
      | right _ => filesystem_lookup_typical rest p
      | left  H => archive_lookup a (subtract p m H)
      end    
  end.
5
In other words, at most one archive is checked for objects.
6
The procedure that jvvfs uses to locate filesystem objects is the source of the term "union": With multiple directories overlapping in different archives, the set of visible files is the union of those in the mounted archives. Directories and files can be hidden by files in more recently mounted archives, but a directories can never hide other directories.
3.5.3
Directory Listing
1
Listing directories proceeds in a similar manner to file lookups.
2
When attempting to list a directory in the filesystem at a given path p, p is first looked up to ensure that it is a directory as are all of its ancestors. If this is not the case, an error is returned.
3
Then, each archive a in the list of archives is considered in turn, starting with the most recently mounted first. The listing procedure begins with an empty set of names S and takes the following steps:
3.5.3.1. Filesystem directory list union
  1. If a is mounted at a path m such that is_ancestor_of m p or m = p, then the object at subtract p m is looked up in a, and a is said to have been checked. Otherwise, the next archive in the list is considered.
  2. If a returns a reference to a directory, then the names in the directory at subtract p m are added to S and the next archive is considered.
  3. If, in a, either subtract p m or an ancestor q of subtract p m is a file, then the contents of subtract p m are said to be shadowed. If shadowing is occuring, and a is not the first archive in the list that has been checked so far, then S is returned and no further archives are considered. Otherwise, an error is returned (indicating that q is not a directory).
3.5.3.2. Filesystem directory list union (Coq)
Require Coq.Arith.Peano_dec.
Require Coq.Lists.ListSet.

Axiom name_eq_dec : forall (n m : name),
  {n = m}+{n <> m}.

Fixpoint filesystem_directory_list_union'
  (archives : list archive)
  (p        : path_virtual)
  (checks   : nat)
  (current  : ListSet.set name)
: io error_code (list name) :=
  match archives with
  | nil         => Success _ _ current
  | cons a rest =>
    let m := archive_mount a in
      match ancestor_or_equal m p with
      | right _ => filesystem_directory_list_union' rest p checks current
      | left  H =>
        match archive_directory_list a (subtract p m H) with
        | Success names                => filesystem_directory_list_union' rest p (S checks) (ListSet.set_union name_eq_dec current names)
        | Failure FSErrorNotADirectory =>
          if Peano_dec.eq_nat_dec checks 0
          then Failure _ _ FSErrorNotADirectory
          else Success _ _ current
        | Failure e => Failure _ _ e
        end
      end
  end.

Definition filesystem_directory_list_union
  (archives : list archive)
  (p        : path_virtual)
:= filesystem_directory_list_union' archives p 0 nil.

Definition filesystem_directory_list
  (archives : list archive)
  (p        : path_virtual)
: io error_code (list name) :=
  match filesystem_lookup archives p with
  | Success None                        => Failure _ _ FSErrorNotADirectory
  | Success (Some FSReferenceFile)      => Failure _ _ FSErrorNotADirectory
  | Success (Some FSReferenceDirectory) => filesystem_directory_list_union archives p
  | Failure e                           => Failure _ _ e
  end.
4
Rationale
4.1
Why not Java resources?
1
Java resources allow developers to access program resources and data files without explicit access to a filesystem. This is usually sufficient if all the resources in question are conceptually part of the program. The main problem that jvvfs attempts to solve is the problem of the set of required resources not being known or available on program startup.
2
Consider a game or simulation that allows the loading of third-party levels or other assets. The OpenTTD engine is a good example of this, as it comes with a built-in installer for third party content:
4.1.1. OpenTTD content installer
OpenTTD content installer
3
Implementing the above with Java resources turns out to be rather complicated. Overriding resources (to allow for content "upgrades") is equally difficult.
4
The jvvfs package provides a uniform namespace for all resources, and new resources can be added at any time by simply adding new archives and/or directories to the archive directory and then mounting them as explained elsewhere in this documentation. The actual downloading of external resource archives is considered to be outside of the scope of jvvfs and can be easily provided by classes in the Java standard library.
5
API Reference
5.1
Javadoc
1
API documentation for the package is provided via the included Javadoc.
6
Listings
6.1
Specifications
6.1.1. Specification listings
6.2
Examples
6.2.1. Example listings
[0]
http://semver.org
[1]
http://en.wikipedia.org/wiki/Zip_(file_format)
[2]
http://io7m.com/software/jlog
[3]
http://en.wikipedia.org/wiki/Command_line_completion
[4]
http://coq.inria.fr
[5]
http://en.wikipedia.org/wiki/EBNF