Two weeks ago, I assigned homework. Rewrite the .NET Socket API so that you can prove the following assertions:

• You cannot use a Socket returned from Accept to accept any additional connections from the connection queue.
• You cannot call Accept, Bind, Connect, Listen, Receive, or Send if the socket has been closed.
• You must call Bind before you can call the Listen method.
• You must call Listen before calling Accept.
• Connect(string host, int port) can only be called if addressFamily is either InterNetwork or InterNetworkV6.
• Connect cannot be called if Listen has been called.
• You have to either call Connect or Accept before Sending and Receiving data.
• If the socket has been previously disconnected, then you cannot use Connect to restore the connection.

These assertions are prominently listed in the MSDN documentation. Why not roll them into the API itself? Let the compiler prove that we are using sockets correctly. Last week, I gave you a hint. I moved the Send and Receive methods out to a different class so that we can prove that you've called Accept or Connect prior to Send or Receive. Both Accept and Connect became factory methods. You must call the factory before you get the object, and you must get the object before you call its methods. Q.E.D. Let's start from there and prove the rest of the assertions. Starting point

• You have to either call Connect or Accept before Sending and Receiving data.

public class ConnectedSocket
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
}

public class Socket : IDisposable
{
    public Socket(SocketInformation socketInformation);
    public Socket(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public ConnectedSocket Accept();
    public void Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
    public void Dispose();
    public void Listen(int backlog);
}

Looking through the list of assertions, we find that this one is already taken care of by the first change:

• You cannot use a Socket returned from Accept to accept any additional connections from the connection queue.

The ConnectedSocket class doesn't have an Accept method, so you can't call it. Q.E.D.
Other prerequisitesThere are three other prerequisite assertions that we can prove in exactly the same way:

• You must call Bind before you can call the Listen method.
• You must call Listen before calling Accept.
• Connect cannot be called if Listen has been called.

public class Socket : IDisposable
{
    public Socket(SocketInformation socketInformation);
    public Socket(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public BoundSocket Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
    public void Dispose();
}

public class BoundSocket
{
    public ListeningSocket Listen(int backlog);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
}

public class ListeningSocket
{
    public ConnectedSocket Accept();
}

Bind becomes a factory for the class that gives you Listen. Bind does not take away your ability to call Connect. Listen does.
Factory and productFactories are great prerequisites. Now that it is becoming more obvious that we are using that pattern, let's rename Socket and move IDisposable to the product.

public class SocketFactory
{
    public SocketFactory(SocketInformation socketInformation);
    public SocketFactory(AddressFamily addressFamily, SocketType socketType, ProtocolType protocolType);

    public BoundSocket Bind(EndPoint localEP);
    public ConnectedSocket Connect(EndPoint remoteEP);
    public ConnectedSocket Connect(string host, int port);
}

public class ConnectedSocket : IDisposable
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
    public void Dispose();
}

The ConnectedSocket is the ultimate product. That's the socket that needs to be closed. And what do you know, this change proves another of our assertions:

• If the socket has been previously disconnected, then you cannot use Connect to restore the connection.

It is impossible to call Connect on a socket that has been disposed, since they aren't the same object anymore.
Dispose onceNow that the Dispose method is where it belongs, let's focus on the assertion most concerned with its use:

• You cannot call Accept, Bind, Connect, Listen, Receive, or Send if the socket has been closed.

Accept, Bind, Connect, and Listen have already been taken care of, since they have become factory methods. To handle Send and Receive, we turn every ConnectedSocket factory into a callback:

public class ConnectedSocket
{
    public int Receive(byte[] buffer);
    public int Send(byte[] buffer);
}

public void Connect(string host, int port, Action<ConnectedSocket> action);

We have taken away the capability of disposing a socket. The factory does it on the consumer's behalf. Since there is no way for the consumer to call Dispose, and since the callback returns before Dispose is called, there is no way to call Send or Receive after Dispose. Q.E.D.
Specialized factoryWhich leaves us with one final assertion:

• Connect(string host, int port) can only be called if addressFamily is either InterNetwork or InterNetworkV6.

Again, we want to move the restricted method into its own special class. But now, we want to enforce that certain values are provided, not that certain methods are called. We'll limit this by creating our own smaller enumeration.

public class IPSocketFactory : SocketFactory
{
    public enum Version { V4, V6 }
    public IPSocketFactory(Version version, SocketType socketType, ProtocolType protocolType)
        : base(
            version == Version.V4 ? AddressFamily.InterNetwork : AddressFamily.InterNetworkV6,
            socketType,
            protocolType) { }

    public void Connect(string host, int port, Action<ConnectedSocket> action);
}

If you want to call the Connect overload with two parameters, you have to use the limited enumeration to get the right factory. I didn't mess with the overloaded constructor, because it complicates things.
One slight wrinkle. In a previous change we created a copy of the Connect method, since it can be called after Bind(). So we make the same change there:

public class IPBoundSocket : BoundSocket
{
    public void Connect(string host, int port, Action<ConnectedSocket> action);
}

public class IPSocketFactory : SocketFactory
{
    public enum Version { V4, V6 }
    public IPSocketFactory(Version version, SocketType socketType, ProtocolType protocolType)
        : base(
            version == Version.V4 ? AddressFamily.InterNetwork : AddressFamily.InterNetworkV6,
            socketType,
            protocolType) { }

    public IPBoundSocket Bind(EndPoint localEP);
    public void Connect(string host, int port, Action<ConnectedSocket> action);
}

The only way to get an IPBoundSocket is to use the IPSocketFactory. Therefore, you must have selected one of the Internet protocols. By the way, this is taking advantage of a little-used feature of C# called covarience. This is the one part of the proof that might not work in other languages.
So there you have it. A provably correct Socket API. There is no way to use it incorrectly. The compiler enforces all of the assertions that we would otherwise have to read the documentation to discover.