none
Constructors chaining

    질문

  • 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



    • 편집됨 Eyal Shilony 2012년 7월 24일 화요일 오후 10:02
    2012년 7월 24일 화요일 오후 9:53

답변

  • 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

    • 답변으로 제안됨 Raphael Schweizer 2012년 8월 3일 금요일 오후 2:35
    • 답변으로 표시됨 Eyal Shilony 2012년 8월 3일 금요일 오후 4:53
    2012년 7월 26일 목요일 오전 10:34
  • 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
    • 답변으로 표시됨 Eyal Shilony 2012년 8월 3일 금요일 오후 4:53
    2012년 8월 3일 금요일 오후 2:35

모든 응답

  • 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

    • 답변으로 제안됨 Raphael Schweizer 2012년 8월 3일 금요일 오후 2:35
    • 답변으로 표시됨 Eyal Shilony 2012년 8월 3일 금요일 오후 4:53
    2012년 7월 26일 목요일 오전 10:34
  • 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


    • 편집됨 Eyal Shilony 2012년 7월 26일 목요일 오후 12:54
    2012년 7월 26일 목요일 오후 12:53
  • 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
    • 답변으로 표시됨 Eyal Shilony 2012년 8월 3일 금요일 오후 4:53
    2012년 8월 3일 금요일 오후 2:35
  • 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

    2012년 8월 3일 금요일 오후 4:53