From 817b3ee128e905cdb965411aea159aedbb6fcdd5 Mon Sep 17 00:00:00 2001 From: Nathan Dykman Date: Mon, 12 Sep 2016 16:04:24 -0700 Subject: [PATCH] Minor fixes to the contracts --- .../System.Windows.Forms.ColorDialog.cs | 4 --- .../System.Windows.Forms.FileDialog.cs | 25 ++++++++++++------- 2 files changed, 16 insertions(+), 13 deletions(-) diff --git a/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ColorDialog.cs b/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ColorDialog.cs index d0c64d3e..b3a81af6 100644 --- a/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ColorDialog.cs +++ b/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.ColorDialog.cs @@ -68,10 +68,6 @@ namespace System.Windows.Forms Contract.Ensures(Contract.Result() != null); return default(int[]); } - set - { - - } } // diff --git a/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.FileDialog.cs b/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.FileDialog.cs index 316e45b9..ffbda800 100644 --- a/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.FileDialog.cs +++ b/Microsoft.Research/Contracts/System.Windows.Forms/System.Windows.Forms.FileDialog.cs @@ -70,15 +70,22 @@ namespace System.Windows.Forms // // public bool DereferenceLinks {get; set;} - // - // Gets or sets a string containing the file name selected in the file dialog box. - // - // - // - // The file name selected in the file dialog box. The default value is an empty string (""). - // - // - // public string FileName {get; set;} + /// + /// Gets or sets a string containing the file name selected in the file dialog box. + /// + /// + /// + /// The file name selected in the file dialog box. The default value is an empty string (""). + /// + /// + public string FileName + { + get + { + Contract.Ensures(Contract.Result() != null); + return default(string); + } + } /// /// Gets the file names of all selected files in the dialog box.