Section: 99 [filesys.ts::fs.op.last_write_time] Status: NAD Submitter: GB-15 Opened: 2014-01-20 Last modified: 2016-08-10
Priority: Not Prioritized
View all other issues in [filesys.ts::fs.op.last_write_time].
View all issues with NAD status.
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
[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.
[2014-02-13 LWG/SG-3 Issaquah: No consensus for change.]