Method: VERSION-CONTROL
  Preconditions:
    (DAV:cannot-add-to-existing-history)
    (DAV:must-be-version)
    (DAV:one-version-controlled-resource-per-history-per-workspace)
    (DAV:cannot-modify-checked-in-parent)
  Postconditons:
    (DAV:put-under-version-control)
    (DAV:must-not-change-existing-checked-in-out)
    (DAV:new-version-history)
    (DAV:new-version-controlled-resource)
    (DAV:new-version-controlled-collection)

Method: REPORT
  Preconditions:
    (DAV:supported-report)
    (DAV:acceptable-depth)
  Postconditions:
    (DAV:no-modification)

Method: REPORT (DAV:locate-by-history)
  Preconditions:
    (DAV:must-be-version-history)

Method: REPORT (DAV:compare-baseline)
  Preconditions:
    (DAV:must-be-baseline)
    (DAV:baselines-from-same-history)

Method: REPORT (DAV:latest-activity-version)
  Preconditions:
    (DAV:must-be-activity)

Method: PUT
  Preconditions:
    (DAV:cannot-modify-version-controlled-content)
    (DAV:cannot-modify-version)
  Postconditions:
    (DAV:auto-checkout)
    (DAV:auto-checkout-checkin)

Method: PROPFIND
  Preconditions:
    (DAV:supported-live-property)

Method: PROPPATCH
  Preconditions:
    (DAV:cannot-modify-version-controlled-property)
    (DAV:cannot-modify-version)
    (DAV:cannot-modify-protected-property)
    (DAV:supported-live-property)
  Postconditions:
    (DAV:auto-checkout)
    (DAV:auto-checkout-checkin)

Method: DELETE
  Preconditions:
    (DAV:no-version-delete)
    (DAV:cannot-modify-checked-in-parent)
  Postconditions:
    (DAV:update-predecessor-set)
    (DAV:delete-version-set)
    (DAV:version-history-has-root)
    (DAV:delete-workspace-members)
    (DAV:delete-version-reference)
    (DAV:delete-activity-reference)
    (DAV:delete-working-collection-binding)

Method: COPY
  Preconditions:
    (*** all-off-version-control ***)
    (DAV:cannot-copy-history)
    (DAV:cannot-copy-collection-version)
  Postconditions:
    (DAV:must-not-copy-versioning-property)
    (DAV:auto-checkout)
    (DAV:auto-checkout-checkin)
    (DAV:copy-creates-new-resource)
    (DAV:copy-creates-new-resource)
    (*** all-of-baseline-control ***)

Method: MOVE
  Preconditions:
    (DAV:cannot-rename-version)
    (DAV:cannot-rename-history)
    (DAV:cannot-rename-working-resource)
    (DAV:cannot-modify-checked-in-parent)
    (DAV:cannot-modify-destination-checked-in-parent)
  Postconditions:
    (DAV:preserve-versioning-properties)
    (DAV:workspace-member-moved)
    (DAV:workspace-moved)
    (DAV:update-auto-update)
    (DAV:update-checked-out-reference)
    (DAV:update-activity-reference)
    (DAV:update-workspace-reference)

Method: UNLOCK
  Preconditions:
    (DAV:version-history-is-tree)
  Postconditions:
    (DAV:auto-checkin)

Method: CHECKOUT (applied to a version-controlled resource)
  Preconditions:
    (DAV:must-be-checked-in)
    (DAV:checkout-of-version-with-descendant-is-forbidden)
    (DAV:checkout-of-version-with-descendant-is-discouraged)
    (DAV:checkout-of-checked-out-version-is-forbidden)
    (DAV:checkout-of-checked-out-version-is-discouraged)
    (DAV:must-not-update-baseline-collection)
    (DAV:one-checkout-per-activity-per-history)
    (DAV:linear-activity)
  Postconditions:
    (DAV:is-checked-out)
    (DAV:initialize-predecessor-set)
    (DAV:initialize-activity-set)
    (DAV:initialize-unreserved)
    (DAV:initialize-version-history-bindings)

Method: CHECKOUT (applied to a version)
  Preconditions:
    (DAV:checkout-of-version-with-descendant-is-forbidden)
    (DAV:checkout-of-version-with-descendant-is-discouraged)
    (DAV:checkout-of-checked-out-version-is-forbidden)
    (DAV:checkout-of-checked-out-version-is-discouraged)
  Postconditions:
    (DAV:create-working-resource)
    (DAV:create-working-resource-from-checked-in-version)

Method: CHECKIN (applied to a version-controlled resource)
  Preconditions:
    (DAV:must-be-checked-out)
    (DAV:version-history-is-tree) The versions identified by the DAV:predecessor-set of the checked-out resource MUST be descendants of the root version of the version history for the DAV:checked-out version.
    (DAV:checkin-fork-forbidden)
    (DAV:checkin-fork-discouraged)
    (DAV:merge-must-be-complete)
    (DAV:no-checked-out-baseline-controlled-collection-members)
    (DAV:one-version-per-history-per-baseline)
    (DAV:cannot-modify-version-controlled-configuration)
    (DAV:linear-activity)
    (DAV:atomic-activity-checkin)
  Postconditions:
    (DAV:create-version)
    (DAV:initialize-version-content-and-properties)
    (DAV:checked-in)
    (DAV:keep-checked-out)
    (DAV:add-to-history)
    (DAV:create-baseline-collection)
    (DAV:modify-configuration)
    (DAV:initialize-activity-set)
    (DAV:activity-checkin)
    (DAV:initialize-version-controlled-bindings)
    (DAV:version-control-working-collection-members)

Method: CHECKIN (applied to a working resource)
  Preconditions:
    (DAV:must-be-checked-out)
    (DAV:version-history-is-tree) See Section 4.4.
    (DAV:checkin-fork-forbidden)
    (DAV:checkin-fork-discouraged)
    (DAV:no-overwrite-by-auto-update)
  Postconditions:
    (DAV:create-version)
    (DAV:initialize-version-content-and-properties)
    (DAV:auto-update)
    (DAV:delete-working-resource)

Method: UNCHECKOUT
  Preconditions:
    (DAV:must-be-checked-out-version-controlled-resource)
  Postconditions:
    (DAV:cancel-checked-out)
    (DAV:restore-content-and-dead-properties)
    (DAV:update-version-controlled-collection-members)

Method: MKWORKSPACE
  Preconditions:
    (DAV:resource-must-be-null)
    (DAV:workspace-location-ok)
  Postconditions:
    (DAV:initialize-workspace)

Method: UPDATE
  Preconditions:
    (DAV:must-be-checked-in)
    (DAV:baseline-controlled-members-must-be-checked-in)
    (DAV:must-not-update-baseline-collection)
    (DAV:cannot-modify-version-controlled-configuration)
    (DAV:must-select-version-in-history)
    (DAV:depth-update)
  Postconditions:
    (DAV:update-content-and-properties)
    (DAV:report-properties)
    (DAV:set-baseline-controlled-collection-members)
    (DAV:update-subbaselines)
    (DAV:modify-configuration)
    (DAV:update-version-controlled-collection-members)
    (DAV:apply-request-to-labeled-version)

Method: LABEL
  Preconditions:
    (DAV:must-be-checked-in)
    (DAV:add-must-be-new-label)
    (DAV:label-must-exist)
  Postconditions:
    (DAV:add-or-set-label)
    (DAV:remove-label)

Method: MERGE
  Preconditions:
    (DAV:cannot-merge-checked-out-resource)
    (DAV:checkout-not-allowed)
    (DAV:must-not-update-baseline-collection)
    (DAV:cannot-modify-version-controlled-configuration)
  Postconditions:
    (DAV:ancestor-version)
    (DAV:descendant-version)
    (DAV:checked-out-for-merge)
    (DAV:update-merge-set)
    (DAV:report-properties)
    (DAV:merge-baseline)
    (DAV:merge-subbaselines)
    (DAV:set-baseline-controlled-collection-members)
    (DAV:modify-configuration)
    (DAV:checkin-activity)
    (DAV:update-version-controlled-collection-members)

Method: BASELINE-CONTROL
  Preconditions:
    (DAV:version-controlled-configuration-must-not-exist)
    (DAV:must-be-baseline)
    (DAV:must-have-no-version-controlled-members)
    (DAV:one-baseline-controlled-collection-per-history-per-workspace)
  Postconditions:
    (DAV:create-version-controlled-configuration)
    (DAV:reference-version-controlled-configuration)
    (DAV:select-existing-baseline)
    (DAV:create-new-baseline)

Method: MKCOL
  Preconditions:
    (*** all-of-version-control ***)
  Postconditions:
    (*** all-of-baseline-control ***)
    (*** all-of-version-control ***)

Method: MKACTIVITY
  Preconditions:
    (DAV:resource-must-be-null)
    (DAV:activity-location-ok)
  Postconditions:
    (DAV:initialize-activity)