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

Section: 15.25 [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.

Discussion:

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

[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.]

Proposed resolution: