Constructors chaining

Question

Hello,

I have the following base class

public abstract class ShallowFileSystem : IFileSystemInfo
{
	protected ShallowFileSystem(FileSystemInfo fileSystemInfo)
	{
		Contract.Requires(fileSystemInfo != null);
		Contract.Requires(!string.IsNullOrEmpty(fileSystemInfo.Name));
		Contract.Requires(!string.IsNullOrEmpty(fileSystemInfo.FullName));

		FileSystem = fileSystemInfo;
	}
	
	// ...
}

and in my derived class I have the following constructor that takes a fileName the problem is that I cannot verify the Name and FullName properties.

public class ShallowFileInfo : ShallowFileSystem, IFileInfo
{
	public ShallowFileInfo(string fileName)
		: this(new FileInfo(fileName)) 
	{
		Contract.Requires(!string.IsNullOrEmpty(fileName));
	}

	public ShallowFileInfo(FileInfo fileInfo)
		: base(fileInfo)
	{
		Contract.Requires(fileInfo != null);
		Contract.Requires(!string.IsNullOrEmpty(fileInfo.Name));
		Contract.Requires(!string.IsNullOrEmpty(fileInfo.FullName));

		File = fileInfo;
	}
	
	// ...
}

I'm getting the following errors.

Warning    CodeContracts: requires unproven: !string.IsNullOrEmpty(fileInfo.Name)    e:\Projects\Visual Studio\EasyFront\Source\Framework\EasyFront.Framework\IO\ShallowFileInfo.cs    19    EasyFront.Framework
Warning    CodeContracts: requires unproven: !string.IsNullOrEmpty(fileInfo.FullName)    e:\Projects\Visual Studio\EasyFront\Source\Framework\EasyFront.Framework\IO\ShallowFileInfo.cs    19    EasyFront.Framework

EDIT: One solution that I came up with is using a factory method like this.

public static IDirectoryInfo Create(string path)
		{
			Contract.Requires(!string.IsNullOrEmpty(path));

			DirectoryInfo directoryInfo = new DirectoryInfo(path);

			Assert.NotNullOrEmpty(directoryInfo.Name);
			Assert.NotNullOrEmpty(directoryInfo.FullName);

			return new ShallowDirectoryInfo(directoryInfo);
		}

---

Regards,

Eyal Shilony

Answer 1

In your ShallowFileInfo class could you not have a static method and do it like so:

public class ShallowFileInfo : ShallowFileSystem, IFileInfo
{
    public ShallowFileInfo(string fileName)
        : this(CreateFileInfo(fileName)) 
    {
        Contract.Requires(!string.IsNullOrEmpty(fileName));
    }
    
    public ShallowFileInfo(FileInfo fileInfo)
        : base(fileInfo)
    {
        Contract.Requires(fileInfo != null);
        Contract.Requires(!string.IsNullOrEmpty(fileInfo.Name));
        Contract.Requires(!string.IsNullOrEmpty(fileInfo.FullName));
        
        File = fileInfo;
    }
    
    private static FileInfo CreateFileInfo(string path)
    {
        Contract.Ensures(Contract.Result<FileInfo>() != null);
        Contract.Ensures(!string.IsNullOrEmpty(Contract.Result<FileInfo>().Name));
        Contract.Ensures(!string.IsNullOrEmpty(Contract.Result<FileInfo>().FullName));
        
        var fileInfo = new FileInfo(path);
        Contract.Assume(!string.IsNullOrEmpty(fileInfo.Name));
        Contract.Assume(!string.IsNullOrEmpty(fileInfo.FullName));
        
        return fileInfo;
    }
    
    // ...
}

It might be worth asking the code contracts team to add these Ensures directly to FileInfo.Name and FileInfo.FullName if possible.

Regards,

Luke

Answer 2

The problem with it is that it doesn't satisfy the invariant so you end up with the following warning 'invariant is false: File != null'.

---

Regards,

Eyal Shilony

Answer 3

I couldn't reproduce the warning. Why should it be emitted? The CreateFileInfo method is static, so has no knowledge of the (assumed) File property...

Could you post a more complete example? The following gives no warning for me:

namespace Terminal
{
    using System.Diagnostics.Contracts;
    using System.IO;

    public class ShallowFileInfo : ShallowFileSystem
    {
        public static void Main(string[] args)
        {
            new ShallowFileInfo("non-empty");
        }

        public FileInfo File { get; private set; }

        public ShallowFileInfo(string fileName)
            : this(CreateFileInfo(fileName))
        {
            Contract.Requires(!string.IsNullOrEmpty(fileName));
        }

        public ShallowFileInfo(FileInfo fileInfo)
            : base(fileInfo)
        {
            Contract.Requires(fileInfo != null);
            Contract.Requires(!string.IsNullOrEmpty(fileInfo.Name));
            Contract.Requires(!string.IsNullOrEmpty(fileInfo.FullName));

            File = fileInfo;
        }

        private static FileInfo CreateFileInfo(string path)
        {
            Contract.Requires(!string.IsNullOrEmpty(path));
            Contract.Ensures(Contract.Result<FileInfo>() != null);
            Contract.Ensures(!string.IsNullOrEmpty(Contract.Result<FileInfo>().Name));
            Contract.Ensures(!string.IsNullOrEmpty(Contract.Result<FileInfo>().FullName));

            var fileInfo = new FileInfo(path);
            Contract.Assume(!string.IsNullOrEmpty(fileInfo.Name));
            Contract.Assume(!string.IsNullOrEmpty(fileInfo.FullName));

            return fileInfo;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(File != null);
        }
    }

    public abstract class ShallowFileSystem
    {
        public FileSystemInfo FileSystem { get; private set; }

        protected ShallowFileSystem(FileSystemInfo fileSystemInfo)
        {
            Contract.Requires(fileSystemInfo != null);
            Contract.Requires(!string.IsNullOrEmpty(fileSystemInfo.Name));
            Contract.Requires(!string.IsNullOrEmpty(fileSystemInfo.FullName));

            FileSystem = fileSystemInfo;
        }
    }
}

- Raphael

Answer 4

I gave it another try and you're right, it's actually working! I already tried it once and probably missed one of the ensures so I moved to the next item and left it completely. :)

Thank you both.

---

Regards,

Eyal Shilony