Permalink
Browse files

Contract fixes and transfer updates

  • Loading branch information...
1 parent b8171c3 commit 72f708d7196ed7474fde6db883132f783286e7bb @Strilanc committed Jul 5, 2011
View
1 Bnet/ClientAuthenticator.vb
@@ -73,7 +73,6 @@ Namespace Bnet
Me._privateKey = privateKey
Me._publicKey = BigInteger.ModPow(G, _privateKey, N)
Contract.Assume(_publicKey >= 0)
- Contract.Assume(Me.UserName = _userName)
End Sub
''' <summary>Creates client credentials for the given username and password, with a public/private key pair generated using the given random number generator.</summary>
''' <param name="username">The client's username.</param>
View
1 Bnet/Protocol/TextHexValueJar.vb
@@ -35,7 +35,6 @@ Namespace Bnet.Protocol
Return _digitCount
End Get
End Property
- <SuppressMessage("Microsoft.Contracts", "Ensures-47-18")>
Protected Overrides Function FixedSizeParse(data As IRist(Of Byte)) As UInteger
Return CUInt(data.ToAsciiChars.FromHexToUInt64(_byteOrder))
End Function
View
3 Commands/CommandArgument.vb
@@ -71,9 +71,6 @@ Namespace Commands
''' Splits text into tokens separated by spaces and fused by brackets.
''' </summary>
<Pure()>
- <SuppressMessage("Microsoft.Contracts", "Requires-45-104")>
- <SuppressMessage("Microsoft.Contracts", "Requires-45-239")>
- <SuppressMessage("Microsoft.Contracts", "Requires-45-389")>
Public Shared Function Tokenize(text As String) As IEnumerable(Of String) 'verification disabled due to stupid verifier
Contract.Requires(text IsNot Nothing)
Contract.Ensures(Contract.Result(Of IEnumerable(Of String))() IsNot Nothing)
View
110 Components/IBotComponent.vb
@@ -1,5 +1,5 @@
Namespace Components
- <ContractClass(GetType(IBotComponent.ContractClass))>
+ <ContractClass(GetType(ContractClassIBotComponent))>
Public Interface IBotComponent
Inherits IDisposableWithTask
ReadOnly Property Name As InvariantString
@@ -12,68 +12,68 @@
Function InvokeCommand(user As BotUser, argument As String) As Task(Of String)
'''<summary>Adds a command to the component and returns an IDisposable that removes the command upon disposal.</summary>
Function IncludeCommand(command As Commands.ICommand(Of IBotComponent)) As Task(Of IDisposable)
+ End Interface
- <ContractClassFor(GetType(IBotComponent))>
- MustInherit Shadows Class ContractClass
- Implements IBotComponent
-
- Public ReadOnly Property Logger As Logger Implements IBotComponent.Logger
- Get
- Contract.Ensures(Contract.Result(Of Logger)() IsNot Nothing)
- Throw New NotSupportedException
- End Get
- End Property
-
- Public ReadOnly Property HasControl As Boolean Implements IBotComponent.HasControl
- Get
- Throw New NotSupportedException
- End Get
- End Property
- Public ReadOnly Property Control() As Control Implements IBotComponent.Control
- Get
- Contract.Requires(DirectCast(Me, IBotComponent).HasControl)
- Contract.Ensures(Contract.Result(Of Control)() IsNot Nothing)
- Throw New NotSupportedException
- End Get
- End Property
+ <ContractClassFor(GetType(IBotComponent))>
+ Public MustInherit Class ContractClassIBotComponent
+ Implements IBotComponent
- Public Function InvokeCommand(user As BotUser, argument As String) As Task(Of String) Implements IBotComponent.InvokeCommand
- Contract.Requires(argument IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task(Of String))() IsNot Nothing)
+ Public ReadOnly Property Logger As Logger Implements IBotComponent.Logger
+ Get
+ Contract.Ensures(Contract.Result(Of Logger)() IsNot Nothing)
Throw New NotSupportedException
- End Function
+ End Get
+ End Property
- <Pure()>
- Public Function IsArgumentPrivate(argument As String) As Boolean Implements IBotComponent.IsArgumentPrivate
- Contract.Requires(argument IsNot Nothing)
+ Public ReadOnly Property HasControl As Boolean Implements IBotComponent.HasControl
+ Get
Throw New NotSupportedException
- End Function
+ End Get
+ End Property
+ Public ReadOnly Property Control() As Control Implements IBotComponent.Control
+ Get
+ Contract.Requires(DirectCast(Me, IBotComponent).HasControl)
+ Contract.Ensures(Contract.Result(Of Control)() IsNot Nothing)
+ Throw New NotSupportedException
+ End Get
+ End Property
- Public ReadOnly Property Name As InvariantString Implements IBotComponent.Name
- Get
- Throw New NotSupportedException
- End Get
- End Property
- Public ReadOnly Property Type As InvariantString Implements IBotComponent.Type
- Get
- Throw New NotSupportedException
- End Get
- End Property
+ Public Function InvokeCommand(user As BotUser, argument As String) As Task(Of String) Implements IBotComponent.InvokeCommand
+ Contract.Requires(argument IsNot Nothing)
+ Contract.Ensures(Contract.Result(Of Task(Of String))() IsNot Nothing)
+ Throw New NotSupportedException
+ End Function
- Public ReadOnly Property DisposalTask As Task Implements IDisposableWithTask.DisposalTask
- Get
- Throw New NotSupportedException
- End Get
- End Property
- Public Sub Dispose() Implements IDisposable.Dispose
+ <Pure()>
+ Public Function IsArgumentPrivate(argument As String) As Boolean Implements IBotComponent.IsArgumentPrivate
+ Contract.Requires(argument IsNot Nothing)
+ Throw New NotSupportedException
+ End Function
+
+ Public ReadOnly Property Name As InvariantString Implements IBotComponent.Name
+ Get
+ Throw New NotSupportedException
+ End Get
+ End Property
+ Public ReadOnly Property Type As InvariantString Implements IBotComponent.Type
+ Get
Throw New NotSupportedException
- End Sub
+ End Get
+ End Property
- Public Function IncludeCommand(command As Commands.ICommand(Of IBotComponent)) As Task(Of IDisposable) Implements IBotComponent.IncludeCommand
- Contract.Requires(command IsNot Nothing)
- Contract.Ensures(Contract.Result(Of Task(Of IDisposable))() IsNot Nothing)
+ Public ReadOnly Property DisposalTask As Task Implements IDisposableWithTask.DisposalTask
+ Get
Throw New NotSupportedException
- End Function
- End Class
- End Interface
+ End Get
+ End Property
+ Public Sub Dispose() Implements IDisposable.Dispose
+ Throw New NotSupportedException
+ End Sub
+
+ Public Function IncludeCommand(command As Commands.ICommand(Of IBotComponent)) As Task(Of IDisposable) Implements IBotComponent.IncludeCommand
+ Contract.Requires(command IsNot Nothing)
+ Contract.Ensures(Contract.Result(Of Task(Of IDisposable))() IsNot Nothing)
+ Throw New NotSupportedException
+ End Function
+ End Class
End Namespace
View
4 Library/AsyncViewableCollection.vb
@@ -25,7 +25,6 @@ Public Class ObservableCollection(Of T)
Me.outQueue = If(outQueue, MakeTaskedCallQueue())
End Sub
- <SuppressMessage("Microsoft.Contracts", "Ensures-28-62")>
Public Sub Add(item As T) Implements ICollection(Of T).Add
_items.Add(item)
outQueue.QueueAction(Sub() RaiseEvent Added(item))
@@ -46,7 +45,8 @@ Public Class ObservableCollection(Of T)
Public Function Contains(item As T) As Boolean Implements ICollection(Of T).Contains
Return _items.Contains(item)
End Function
- Public Sub CopyTo(array() As T, arrayIndex As Integer) Implements ICollection(Of T).CopyTo
+ Public Sub CopyTo(array As T(), arrayIndex As Integer) Implements ICollection(Of T).CopyTo
+ If arrayIndex >= array.Length Then Throw New ArgumentException("arrayIndex >= array.Length")
_items.CopyTo(array, arrayIndex)
End Sub
Public ReadOnly Property Count As Integer Implements ICollection(Of T).Count
View
8 Library/Common.vb
@@ -233,12 +233,13 @@ Public Module PoorlyCategorizedFunctions
Return "({0}) {1}".Frmt(ex.GetType.Name, ex.Message)
End Function
+ <SuppressMessage("Microsoft.Contracts", "Requires-56-268")>
Public Function FindFilesMatching(fileQuery As String,
likeQuery As InvariantString,
directory As InvariantString,
- maxResults As Integer) As IList(Of String)
+ maxResults As Integer) As IRist(Of String)
Contract.Requires(fileQuery IsNot Nothing)
- Contract.Ensures(Contract.Result(Of IList(Of String))() IsNot Nothing)
+ Contract.Ensures(Contract.Result(Of IRist(Of String))() IsNot Nothing)
If Not directory.EndsWith(IO.Path.DirectorySeparatorChar) AndAlso Not directory.EndsWith(IO.Path.AltDirectorySeparatorChar) Then
directory += IO.Path.DirectorySeparatorChar
@@ -261,7 +262,7 @@ Public Module PoorlyCategorizedFunctions
Select relativePath = filepath.Substring(directory.Length)
Where relativePath Like likeQuery
Where relativePath Like dirQuery
- ).Take(maxResults).ToList
+ ).Take(maxResults).ToRist()
End Function
Public Function GetDataFolderPath(subfolder As String) As String
Contract.Requires(subfolder IsNot Nothing)
@@ -454,6 +455,7 @@ Public Module PoorlyCategorizedFunctions
).ToRist
End Function
+ <Pure()>
Public Sub CheckIOData(clause As Boolean, message As String)
Contract.Requires(message IsNot Nothing)
Contract.Ensures(clause)
View
1 Pickling/KeyPrefixedJar.vb
@@ -47,7 +47,6 @@ Namespace Pickling
"{0}: {1}".Frmt(keyDesc, valueDesc),
"{0}, {1}".Frmt(keyDesc, valueDesc))
End Function
- <SuppressMessage("Microsoft.Contracts", "Requires-36-179")>
<SuppressMessage("Microsoft.Contracts", "Ensures-28-210")>
Public Overrides Function Parse(text As String) As KeyValuePair(Of TKey, Object)
Dim divider = If(_useSingleLineDescription, ":", ",")
View
4 Pickling/Numeric Jars.vb
@@ -78,7 +78,6 @@
Return 2
End Get
End Property
- <SuppressMessage("Microsoft.Contracts", "Ensures-47-26")>
Protected Overrides Function FixedSizeParse(data As IRist(Of Byte)) As UInt16
Contract.Assume(data.Count = 2)
Return data.ToUInt16(byteOrder)
@@ -203,7 +202,6 @@
Return 8
End Get
End Property
- <SuppressMessage("Microsoft.Contracts", "Ensures-47-26")>
Protected Overrides Function FixedSizeParse(data As IRist(Of Byte)) As UInt64
Contract.Assume(data.Count = 8)
Return data.ToUInt64(byteOrder)
@@ -243,7 +241,6 @@
Return 4
End Get
End Property
- <SuppressMessage("Microsoft.Contracts", "Ensures-47-25")>
Protected Overrides Function FixedSizeParse(data As IRist(Of Byte)) As Single
Dim buffer = data.ToArray()
Contract.Assume(buffer.Length = 4)
@@ -277,7 +274,6 @@
Return 8
End Get
End Property
- <SuppressMessage("Microsoft.Contracts", "Ensures-47-25")>
Protected Overrides Function FixedSizeParse(data As IRist(Of Byte)) As Double
Dim buffer = data.ToArray()
Contract.Assume(buffer.Length = 8)
View
3 Pickling/Pickling Extensions.vb
@@ -31,7 +31,7 @@
End Function
<Extension()> <Pure()>
- <SuppressMessage("Microsoft.Contracts", "Requires-12-59")>
+ <SuppressMessage("Microsoft.Contracts", "Requires-12-64")>
Public Function PackPickle(Of T, TValue As T)(jar As IJar(Of T), value As TValue) As IPickle(Of TValue)
Contract.Requires(jar IsNot Nothing)
Contract.Requires(value IsNot Nothing)
@@ -83,7 +83,6 @@
End If
End Function
<Extension()> <Pure()>
- <SuppressMessage("Microsoft.Contracts", "Requires-45-196")>
Public Function SplitListDescription(text As String, Optional usedSingleLineDescription As Boolean = False) As IEnumerable(Of String)
Contract.Requires(text IsNot Nothing)
Contract.Ensures(Contract.Result(Of IEnumerable(Of String))() IsNot Nothing)
View
2 Tinker.vbproj
@@ -32,7 +32,7 @@
<AssemblyOriginatorKeyFile>StrilancWeak.snk</AssemblyOriginatorKeyFile>
<TargetFrameworkProfile />
<LangVersion />
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
<PublishUrl>C:\Users\Craig\Desktop\Installer\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
View
2 Warcraft3/Download/Download Client.vb
@@ -165,7 +165,7 @@ Namespace WC3.Download
<SuppressMessage("Microsoft.Contracts", "EnsuresInMethod-Contract.Result(Of TransferClient)() Is Nothing OrElse Contract.Result(Of TransferClient)().Transfer Is Nothing")>
<SuppressMessage("Microsoft.Contracts", "EnsuresInMethod-Contract.Result(Of TransferClient)() Is Nothing OrElse Contract.Result(Of TransferClient)().ReportedHasFile")>
<SuppressMessage("Microsoft.Contracts", "EnsuresInMethod-Contract.Result(Of TransferClient)() Is Nothing OrElse Contract.Result(Of TransferClient)().IsSteady")>
- Public Function FindBestAvailableUploader() As TransferClient
+ Public Function TryFindBestAvailableUploader() As TransferClient
Contract.Ensures(Contract.Result(Of TransferClient)() Is Nothing OrElse Contract.Result(Of TransferClient)().HasReported)
Contract.Ensures(Contract.Result(Of TransferClient)() Is Nothing OrElse Contract.Result(Of TransferClient)().Transfer Is Nothing)
Contract.Ensures(Contract.Result(Of TransferClient)() Is Nothing OrElse Contract.Result(Of TransferClient)().ReportedHasFile)
View
47 Warcraft3/Download/Download Manager.vb
@@ -306,33 +306,24 @@ Namespace WC3.Download
''' </summary>
<Pure()>
Private Function TryFindImprovableTransfer() As Transfer
- For Each transfer In From client In AllClients
- Where client.HasReported
- Where Not client.ReportedHasFile
- Where client.Transfer IsNot Nothing
- Order By client.EstimatedBandwidthPerSecond Descending
- Select t = client.Transfer
- Where t.Duration > MinSwitchPeriod
- Where t.ExpectedDurationRemaining > MinSwitchPeriod
- Contract.Assume(transfer IsNot Nothing)
- Dim downloader = transfer.Downloader
- Dim remainingData = _map.FileSize - transfer.ReportedPosition
- Dim curExpectedCost = transfer.ExpectedDurationRemaining.TotalSeconds
-
- 'expected cost of switching and downloading from another uploader
- Dim bestAvailableUploader = downloader.FindBestAvailableUploader()
- If bestAvailableUploader Is Nothing Then Continue For
- Dim newBandwidthPerSecond = Math.Min(downloader.EstimatedBandwidthPerSecond,
- bestAvailableUploader.EstimatedBandwidthPerSecond)
- Dim newExpectedCost = SwitchPenaltyPeriod.TotalSeconds + SwitchPenaltyFactor * remainingData / newBandwidthPerSecond
-
- 'check
- If newExpectedCost < curExpectedCost Then
- Return transfer
- End If
- Next transfer
-
- Return Nothing
+ Return (From client In AllClients
+ Where client.HasReported
+ Where Not client.ReportedHasFile
+ Where client.Transfer IsNot Nothing
+ Let transfer = client.Transfer
+ Where transfer.Duration > MinSwitchPeriod
+ Where transfer.ExpectedDurationRemaining > MinSwitchPeriod
+ Let downloader = transfer.Downloader
+ Let bestAvailableUploader = downloader.TryFindBestAvailableUploader()
+ Where bestAvailableUploader IsNot Nothing
+ Let remainingData = _map.FileSize - transfer.ReportedPosition
+ Let newBandwidthPerSecond = Math.Min(downloader.EstimatedBandwidthPerSecond, bestAvailableUploader.EstimatedBandwidthPerSecond)
+ Let newExpectedCost = SwitchPenaltyPeriod.TotalSeconds + SwitchPenaltyFactor * remainingData / newBandwidthPerSecond
+ Let curExpectedCost = transfer.ExpectedDurationRemaining.TotalSeconds
+ Where newExpectedCost < curExpectedCost
+ Order By client.EstimatedBandwidthPerSecond Descending
+ Select transfer
+ ).FirstOrDefault()
End Function
'''<summary>Starts and stops transfers, trying to minimize the total transfer time.</summary>
@@ -344,7 +335,7 @@ Namespace WC3.Download
Where client.Transfer Is Nothing
Where client.IsSteady
Contract.Assume(downloader IsNot Nothing)
- Dim bestAvailableUploader = downloader.FindBestAvailableUploader()
+ Dim bestAvailableUploader = downloader.TryFindBestAvailableUploader()
If bestAvailableUploader Is Nothing Then Continue For
Contract.Assume(bestAvailableUploader.IsSteady)
Contract.Assume(bestAvailableUploader.HasReported)
View
8 Warcraft3/Download/Download Transfer.vb
@@ -21,10 +21,10 @@ Namespace WC3.Download
End Sub
Public Sub New(downloader As TransferClient,
- uploader As TransferClient,
- startingPosition As UInt32,
- filesize As UInt32,
- clock As IClock)
+ uploader As TransferClient,
+ startingPosition As UInt32,
+ filesize As UInt32,
+ clock As IClock)
Contract.Requires(downloader IsNot Nothing)
Contract.Requires(uploader IsNot Nothing)
Contract.Requires(clock IsNot Nothing)
View
1 Warcraft3/Pinger.vb
@@ -64,7 +64,6 @@
_latency *= 1 - lambda
_latency += lambda * stored.Item2.ElapsedTime.TotalMilliseconds
If _latency <= 0 Then _latency = Double.Epsilon
- Contract.Assume(_latency >= 0)
End Sub
Public Function QueueReceivedPong(salt As UInteger) As Task
Contract.Ensures(Contract.Result(Of Task)() IsNot Nothing)
View
1 Warcraft3/Protocol/GameAction.vb
@@ -81,7 +81,6 @@ Namespace WC3.Protocol
Public Overrides Function SubJar() As IJar(Of KeyValuePair(Of GameActionId, Object))
Return DataJar
End Function
- <SuppressMessage("Microsoft.Contracts", "Ensures-33-18")>
Public Overrides Function PackRaw(value As GameAction) As KeyValuePair(Of GameActionId, Object)
Return value
End Function
View
3 Warcraft3/Protocol/ObjectTypeJar.vb
@@ -20,15 +20,14 @@ Namespace WC3.Protocol
Return "0x{0}".Frmt(value.ToString("X", CultureInfo.InvariantCulture))
End If
End Function
- <SuppressMessage("Microsoft.Contracts", "Ensures-28-263")>
+ <SuppressMessage("Microsoft.Contracts", "Ensures-Contract.Result(Of T)() IsNot Nothing")>
Public Overrides Function Parse(text As String) As UInt32
Try
If text Like New InvariantString("type '????'") Then
Contract.Assume(text.Length >= "type '".Length + "????".Length)
Dim bytes = System.Text.Encoding.ASCII.GetBytes(text.Substring("type '".Length, "????".Length))
Return bytes.ToUInt32(ByteOrder.BigEndian)
ElseIf text Like New InvariantString("0x*") Then
- Contract.Assume(text.Length >= "0x".Length)
Return UInt32.Parse(text.Substring("0x".Length), NumberStyles.HexNumber, CultureInfo.InvariantCulture)
Else
Return UInt32.Parse(text, NumberStyles.Number, CultureInfo.InvariantCulture)
View
1 Warcraft3/Protocol/WC3 Protocol Packers.vb
@@ -170,7 +170,6 @@ Namespace WC3.Protocol
downloader As PlayerId,
uploader As PlayerId,
Optional mapTransferKey As UInt32 = 1) As Packet
- Contract.Requires(filePosition >= 0)
Contract.Requires(fileData IsNot Nothing)
Contract.Requires(downloader <> uploader)
Contract.Ensures(Contract.Result(Of Packet)() IsNot Nothing)
View
2 Warcraft3/Replay/ReplayDataReader.vb
@@ -106,8 +106,6 @@
firstBlockOffset As UInt32,
decompressedSize As UInt32)
Contract.Requires(subStream IsNot Nothing)
- Contract.Requires(blockCount >= 0)
- Contract.Requires(firstBlockOffset >= 0)
Me._stream = subStream
Me._blockCount = blockCount
Me._length = decompressedSize
View
1 Warcraft3/Replay/ReplayEntry.vb
@@ -81,7 +81,6 @@ Namespace WC3.Replay
Public Overrides Function SubJar() As IJar(Of KeyValuePair(Of ReplayEntryId, Object))
Return DataJar
End Function
- <SuppressMessage("Microsoft.Contracts", "Ensures-33-18")>
Public Overrides Function PackRaw(value As ReplayEntry) As KeyValuePair(Of ReplayEntryId, Object)
Return value
End Function
View
6 Warcraft3/W3Map.vb
@@ -333,7 +333,9 @@ Namespace WC3
If Me.FileSize <> stream.Length Then Throw New InvalidStateException("Modified map file.")
Contract.Assume(pos < stream.Length)
stream.Position = pos
- Return stream.Read(CInt(size))
+ Dim r = stream.Read(CInt(size))
+ Contract.Assume(r.Count <= size)
+ Return r
End Using
End Function
@@ -546,7 +548,6 @@ Namespace WC3
Contract.Requires(mapArchive IsNot Nothing)
Contract.Ensures(Contract.Result(Of ReadMapInfoResult)() IsNot Nothing)
- Contract.Assume(mapArchive IsNot Nothing)
Using stream = mapArchive.OpenFileByName("war3map.w3i")
Dim fileFormat = CType(stream.ReadUInt32(), MapInfoFormatVersion)
If Not fileFormat.EnumValueIsDefined Then
@@ -674,6 +675,7 @@ Namespace WC3
team:=0))
Next item
+ Contract.Assume(lobbySlots.Count <= 12)
Contract.Assume(lobbySlots.Count <= rawSlotCount)
CheckIOData(lobbySlots.Count > 0, "Map contains no lobby slots.")
Return lobbySlots.AsRist()

0 comments on commit 72f708d

Please sign in to comment.