Browse files

Contract fixes

  • Loading branch information...
1 parent 5e58e2e commit 7f01b555e8f333448aaaec9ec112f1c80f10b388 @Strilanc committed Jul 7, 2011
View
12 Bnet/Bnet Client.vb
@@ -394,8 +394,8 @@ Namespace Bnet
Private Async Function AwaitReceive(Of T)(packet As Protocol.Packets.Definition(Of T),
Optional ct As Threading.CancellationToken = Nothing) As Task(Of T)
- Contract.Requires(packet IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task(Of T))() IsNot Nothing)
+ Contract.Assume(packet IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task(Of T))() IsNot Nothing)
Dim r = New TaskCompletionSource(Of T)()
Using d1 = IncludeQueuedPacketHandler(packet, Sub(pickle) r.TrySetResult(pickle.Value)),
d2 = ct.Register(Sub() r.TrySetCanceled())
@@ -404,8 +404,8 @@ Namespace Bnet
End Function
Private Async Function ConnectWithAsync(socket As PacketSocket, Optional clientCdKeySalt As UInt32? = Nothing) As Task
- Contract.Requires(socket IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
+ Contract.Assume(socket IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
If Me._state <> ClientState.Disconnected AndAlso Me._state <> ClientState.FinishedInitiatingConnection Then
Throw New InvalidOperationException("Must disconnect before connecting again.")
End If
@@ -461,8 +461,8 @@ Namespace Bnet
End Sub
Private Async Function LogOnAsync(credentials As ClientAuthenticator) As Task
- Contract.Requires(credentials IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
+ Contract.Assume(credentials IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
If _state <> ClientState.EnterUserCredentials Then
Throw New InvalidOperationException("Incorrect state for login.")
End If
View
2 Components/ComponentSet.vb
@@ -37,7 +37,7 @@ Namespace Components
''' Throws an InvalidOperationException if a component with the same name and type identifiers is already included.
''' </summary>
Private Async Sub AddComponent(component As IBotComponent)
- Contract.Requires(component IsNot Nothing)
+ Contract.Assume(component IsNot Nothing)
If _components.Contains(component) Then
Throw New InvalidOperationException("Component already added.")
ElseIf TryFindComponent(component.Type, component.Name).HasValue Then
View
8 Library/Common Async.vb
@@ -91,20 +91,20 @@
Contract.Assume(value IsNot Nothing)
results.Add(value.DisposeAsync())
Next value
- Return TaskEx.WhenAll(results)
+ Return TaskEx.WhenAll(results).AssumeNotNull()
End Function
<Extension()>
Public Function IgnoreExceptions(Of T)(task As TaskCompletionSource(Of T)) As task
Contract.Requires(task IsNot Nothing)
Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
Contract.Assume(task.Task IsNot Nothing)
- Return task.Task.IgnoreExceptions()
+ Return task.Task.IgnoreExceptions().AssumeNotNull()
End Function
<Extension()>
Public Async Function IgnoreExceptions(task As Task) As task
- Contract.Requires(task IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
+ Contract.Assume(task IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
Try
Await task
Catch ex As Exception
View
2 Library/PacketSocket.vb
@@ -152,7 +152,7 @@ Public NotInheritable Class PacketSocket
End Sub
Public Async Function AsyncReadPacket() As Task(Of IRist(Of Byte))
- Contract.Ensures(Contract.Result(Of Task(Of IRist(Of Byte)))() IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task(Of IRist(Of Byte)))() IsNot Nothing)
Try
Dim data = Await packetStreamer.AsyncReadPacket()
If deadManSwitch IsNot Nothing Then deadManSwitch.QueueReset()
View
31 Pickling/Pickling Interfaces.vb
@@ -18,11 +18,42 @@
End Interface
'''<summary>A named jar which parses data and packs values into pickles.</summary>
+ <ContractClass(GetType(ContractClassForINamedJar(Of )))>
Public Interface INamedJar(Of T)
Inherits IJar(Of T)
ReadOnly Property SubJar As IJar(Of T)
ReadOnly Property Name As InvariantString
End Interface
+ <ContractClassFor(GetType(INamedJar(Of )))>
+ Public MustInherit Class ContractClassForINamedJar(Of T)
+ Implements INamedJar(Of T)
+ Public Function Describe(value As T) As String Implements IJar(Of T).Describe
+ Throw New NotImplementedException()
+ End Function
+ Public Function MakeControl() As IValueEditor(Of T) Implements IJar(Of T).MakeControl
+ Throw New NotImplementedException()
+ End Function
+ Public Function Pack(value As T) As LinqToLists.IRist(Of Byte) Implements IJar(Of T).Pack
+ Throw New NotImplementedException()
+ End Function
+ Public Function Parse(data As LinqToLists.IRist(Of Byte)) As ParsedValue(Of T) Implements IJar(Of T).Parse
+ Throw New NotImplementedException()
+ End Function
+ Public Function Parse(text As String) As T Implements IJar(Of T).Parse
+ Throw New NotImplementedException()
+ End Function
+ Public ReadOnly Property Name As Strilbrary.Values.InvariantString Implements INamedJar(Of T).Name
+ Get
+ Throw New NotImplementedException()
+ End Get
+ End Property
+ Public ReadOnly Property SubJar As IJar(Of T) Implements INamedJar(Of T).SubJar
+ Get
+ Contract.Ensures(Contract.Result(Of IJar(Of T))() IsNot Nothing)
+ Throw New NotImplementedException()
+ End Get
+ End Property
+ End Class
<ContractClass(GetType(ISimpleValueEditor.ContractClass))>
Public Interface ISimpleValueEditor
View
4 Warcraft3/Game/W3GameControl.vb
@@ -48,8 +48,8 @@ Namespace WC3
End Sub
Private Async Sub OnGameUpdated(sender As WC3.Game, slots As SlotSet)
- Contract.Requires(sender IsNot Nothing)
- Contract.Requires(slots IsNot Nothing)
+ Contract.Assume(sender IsNot Nothing)
+ Contract.Assume(slots IsNot Nothing)
Dim descriptions = Await TaskEx.WhenAll(From slot In slots Select slot.AsyncGenerateDescription)
inQueue.QueueAction(Sub()
If IsDisposed Then Return
View
8 Warcraft3/Server/GameServer.vb
@@ -189,8 +189,8 @@ Namespace WC3
End Function
Private Async Function AsyncFindPlayer(username As String) As Task(Of Player)
- Contract.Requires(username IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task(Of Player))() IsNot Nothing)
+ Contract.Assume(username IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task(Of Player))() IsNot Nothing)
Dim findResults = Await TaskEx.WhenAll(From entry In _gameSets.Values Select entry.QueueTryFindPlayer(username))
Return (From player In findResults Where player IsNot Nothing).FirstOrDefault
End Function
@@ -200,8 +200,8 @@ Namespace WC3
End Function
Private Async Function AsyncFindPlayerGame(username As String) As Task(Of Game)
- Contract.Requires(username IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task(Of Game))() IsNot Nothing)
+ Contract.Assume(username IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task(Of Game))() IsNot Nothing)
Dim findResults = Await TaskEx.WhenAll(From entry In _gameSets.Values Select entry.QueueTryFindPlayerGame(username))
Return (From game In findResults Where game IsNot Nothing).FirstOrDefault
End Function
View
2 Warcraft3/Server/GameSet.vb
@@ -134,7 +134,7 @@
End Function
Private Async Function AsyncTryFindPlayer(userName As InvariantString) As Task(Of Player)
- Contract.Ensures(Contract.Result(Of Task(Of Player))() IsNot Nothing)
+ 'Contract.Ensures(Contract.Result(Of Task(Of Player))() IsNot Nothing)
Dim findResults = Await TaskEx.WhenAll(From game In _games Select game.QueueTryFindPlayer(userName))
Return (From player In findResults Where player IsNot Nothing).FirstOrDefault
End Function
View
4 Warcraft3/W3Socket.vb
@@ -91,7 +91,9 @@ Namespace WC3
Public Function AsyncReadPacket() As Task(Of IRist(Of Byte))
Contract.Ensures(Contract.Result(Of Task(Of IRist(Of Byte)))() IsNot Nothing)
- Return _socket.AsyncReadPacket()
+ Dim r = _socket.AsyncReadPacket()
+ Contract.Assume(r IsNot Nothing)
+ Return r
End Function
Public ReadOnly Property Socket As PacketSocket
View
1 Warden/Warden Client.vb
@@ -77,6 +77,7 @@
End Try
End Function()
+ Contract.Assume(s IsNot Nothing)
Dim result = New Warden.Client(s, New TaskCompletionSource(Of NoValue), logger)
result.Start()
Return result

0 comments on commit 7f01b55

Please sign in to comment.