Issue 2628: [filesys.ts] [PDTS] Possible last_write_time() postcondition?

Title: [filesys.ts] [PDTS] Possible last_write_time() postcondition?
Status: nad
Section: [fs.op.last_write_time]
Submitter: GB-15

Created on 2014-01-20.00:00:00 last changed 108 months ago

Messages

msg7788 (view)

Date: 2014-02-13.00:00:00

[ 2014-02-13 LWG/SG-3 Issaquah: No consensus for change. ]

msg7787 (view)

Date: 2014-02-15.00:00:00

[ 2014-02-09, Beman Dawes comments: ]

That assumes the file system rounds down. We don't know which direction a file system rounds. Nice try, but this one looks NAD to me.

msg7786 (view)

Date: 2016-01-31.20:31:05

Addresses: filesys.ts

The constraint on last_write_time is too weak: It is noted that the postcondition of last_write_time(p) == new_time is not specified since it might not hold for file systems with coarse time granularity.

However, might it be possible to have a postcondition that last_write_time(p) <= new_time ?

Add postcondition: last_write_time(p) <= new_time

History
Date	User	Action	Args
2016-01-28 01:00:35	admin	set	messages: + msg7788
2016-01-28 01:00:35	admin	set	messages: + msg7787
2014-01-20 00:00:00	admin	create