page 1 of 1
Comments: 1 | Views: 381

Hey I'm new to Spec# and don't even get the very basics...
I'm trying to make a fileloader class which shouldn't be created if the filename is wrong.
I  made the following  (try 1) but get this error about "delayed arguments not matching non-delayed parameters"
The tried to do something about it (try 2), but gets an error about "missing object reference to 'file' "

I'm lost. If anyone could help me out I'll be very happy
Thanks in Advance
Mygind


############## TRY 1 ###############

using System;

using System.IO;

public class FileLoader

{

FileStream file;

StreamReader !stream;

invariant file != null;

public FileLoader(String filename)

{

file = new FileStream(filename, FileMode.Open, FileAccess.Read);

if(file == null){

throw(new MissingFileException("File doesn't exist!"));

}

stream = new StreamReader(file);

}

public string readLine()

{

return stream.ReadLine();

}

~FileLoader()

{

file.Close();

}

}


######## TRY 2 #################

[Microsoft.Contracts.NotDelayed]

public FileLoader(String filename)

{

try{

file = new FileStream(filename, FileMode.Open, FileAccess.Read);

} catch(Exception e){

throw new MissingFileException("File doesn't exist!");

}

if(file == null){

throw(new MissingFileException("File doesn't exist!"));

}

stream = new StreamReader(file);

base();

}

evildictaitor
evildictaitor
How could you use the adjective "indescribable" truthfully?
You seem to be missing one of the important points of Spec# which is that you almost never need to throw an exception - you should do all such things with "requires" and "ensures" contracts.

Secondly you haven't seemed to grasp that

FileStream fs
invariant fs != null

is exactly equivilent to

FileStream! fs;

Thirdly, you should never rely on finalizers to clean up native resources - implement the IDisposable pattern:


using System;
using System.IO;

public class FileLoader : IDisposable
{
FileStream! file;
StreamReader !stream;

public FileLoader(String! filename)
  requires System.File.Exists(filename)
{

file = new FileStream(filename, FileMode.Open, FileAccess.Read);
stream = new StreamReader(file);

}

public string readLine()
{
return stream.ReadLine();
}

#region IDisposable pattern
public void Dispose(){
  Dispose(true);
  GC.SuppressFinalize(this);
}
void Dispose(bool disposing){
   file.Close();
}
~FileLoader(){
  #if DEBUG
    throw new Exception("Always dispose of IDisposable objects manually, or use the using(FileLoader l = new FileLoader()) { ... } pattern");
  #endif
  Dispose(false);
}

#endregion

}

page 1 of 1
Comments: 1 | Views: 381