+
Point of view
All features
class CGI_RESPONSE_CLIENT_REDIRECT_WITH_DOCUMENT
- body_stream /= Void implies body_string /= Void
- content_type /= Void
- is_valid_path(path)
Features
{}
{}
{}
{}
{}
{}
require
-
locked: tagged_out_locked
-
locked: tagged_out_locked
-
locked: tagged_out_locked
ensure
-
still_locked: tagged_out_locked
-
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
-
append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))
require
ensure
- path = a_path.intern
- a_fragment = Void implies fragment = Void
- a_fragment /= Void implies fragment = a_fragment.intern
flush_content_type (a_output:
OUTPUT_STREAM)
effective procedure
{}